Asynchronous Cooperative Contracts for Cooperative Scheduling

Abstract

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.

Publication
In Proc. 17th Intl. Conference on Software Engineering and Formal Methods (SEFM 2019). LNCS 11724. © Springer 2019
Date