Séminaire des équipes de recherche

Generalizing Reduction and Abstraction to Simplify Concurrent Programs: The QED Approach

  • Date : 12/06/2012
  • Lieu : LIP6 Université Pierre et Marie Curie, 4 place Jussieu, 75005, salle 26-00/101
  • Intervenants : Serdar Tasiran - Koç University & Microsoft Research Center for Multi-Core Software Engineering - Istanbul, Turquie
  • Organisateurs : REGAL

A key difficulty in concurrent program verification is the large number of interleavings of fine-grain actions. The typical correctness argument makes use of a separation of concerns. At each phase, one worries only about interference due to concurrency, or the sequential behavior of a code block. We present a proof system, QED, that builds on this intuition. In QED, we formulate semantic conditions under which actions commute, and a somewhat different notion of program abstraction. Commutativity checks between actions and abstraction checks are converted to verification conditions and are checked by the Z3 theorem prover. A key computational advantage is that QED proof steps have locally-checkable antecedents. QED proofs apply reduction and abstraction iteratively and transform a program to consist of larger-grain actions. We show that this approach greatly simplifies proofs of assertions, atomicity and linearizability, even in optimistically concurrent programs.

Mots-clés : LIP6 REGAL

Haut de page

Siège et centres de recherche Inria

Accès direct

Social