Asynchronous Cooperative Contracts for Cooperative Scheduling


Formal specification of multi-threaded programs is notoriously hard, because thread execution may be preempted at any point. In contrast, abstract concurrency models such as actors seriously restrict concurrency to obtain race-free programs. Languages with cooperative scheduling occupy a middle ground between these extremes by explicit scheduling points. They have been used to model complex, industrial concurrent systems. This paper introduces cooperative contracts, a contract-based specification approach for asynchronous method calls in presence of cooperative scheduling. It permits to specify complex concurrent behavior succinctly and intuitively. We design a compositional program logic to verify cooperative contracts and discuss how global analyses can be soundly integrated into the program logic.

In Proc. 17th Intl. Conference on Software Engineering and Formal Methods (SEFM 2019). LNCS 11724. © Springer 2019
Crystal Chang Din
Crystal Chang Din
Assoc. Professor