Owicki Gries Proofs

Project Goal

Define a notion of an Owicki-Gries annotation for a concurrent program, analogously to a Floyd-Hoare annotation for a sequential program. The program is given as a 1-safe Petri net, i.e., threads can be created and destroyed at runtime. Construct Owicki-Gries annotations from a Floyd-Hoare annotation of the product automaton / marking graph. Design techniques to simplify such proofs, i.e., to eliminate ghost variables and simplify the formulae.

Resources

• Original paper by Owicki and Gries: https://dl.acm.org/doi/10.1145/360051.360224
• Verification of Sequential and Concurrent Programs: https://ir.cwi.nl/pub/14569/14569A.pdf

Work Packages

• Formal Definitions & Results
  • Formal definition of an Owicki-Gries annotation for automata.
  • Formal definition of an Owicki-Gries annotation for Petri nets.
  • Program safety theorem base on Owickie-Gries annotations.
• Construction & Simplification
  • Construction from a Floyd-Hoare annotation.
  • Define a notion of the size of an Owicki-Gries annotation.
  • Design simplification methods.
• Ultimate Implementation (branch: wip/dk/owickigries)
  • Setup
  • Owicki-Gries annotation
  • Construction from Floyd-Hoare
  • Validity Check
  • Simplification

Current Tasks

• Find example programs.
• Formally describe construction from Floyd-Hoare. In particular, do we need to use negated ghost variables?
• Implement construction & checking in Ultimate.

Implementation

A preliminary version of the computation of Floyd-Hoare annotations for concurrent programs is now available on the project branch. This can be used as input to the construction of an Owicki-Gries annotation (to be implemented).

The annotation class itself is located in the TraceAbstraction project, in package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.concurrency. The construction is currently located in a static method in this class (to be implemented). The validity check is in a separate class, OwickiGriesValidityCheck (to be implemented) in the same package.

The construction and validity check will be called from the BasicCegarLoop class (de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction), in the method computeOwickiGries.

Debugging

Run Ultimate with the settings in trunk/examples/settings/automizer/concurrent/svcomp-Reach-32bit-Automizer_Default-noMmResRef-FA-NoLbe.epf and the XML toolchain trunk/examples/toolchains/AutomizerBplInline.xml. Use Boogie programs (file extension .bpl).