Annotated transition systems for verifying concurrent programs

• Main Author: Paczkowski, Pawel
• Published: University of Edinburgh 1990
• Subjects: 004.01
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.660279

We propose what we view as a generalization of an assertional approach to the verification of concurrent programs. In doing so we put an emphasis on reflecting the semantic contents of programs rather than their syntax in the adopted pattern of reasoning. Therefore assertions annotate not a text of a program but a transition system which represents an object derived from the operational semantics, the control flow of a program. Unlike in the case of sequential programs, where annotating a program text and its control flow amounts to the same, those two possible patterns of attaching assertions are different in the presence of concurrency. The annotated transition systems (annotations, in short) that we introduce and the satisfaction relation between behaviours and annotations are intended to capture the basic idea of assertional reasoning, i.e. of characterizing the reachable states of computations by assertions and deriving program properties from such characterizations. We emphasize the role of control flow as, on the one hand, a separable ingredient of the operational semantics and, on the other hand, as a major concern in formulating properties of concurrent programs and verifying them. The rigorous definition of control flow proves important for analysing deadlock freedom and mutual exclusion. We develop proof techniques for showing partial correctness, mutual exclusion, deadlock freedom, and termination of concurrent programs. The relative ease in establishing soundness and completeness of the proposed proof methods is due to the fact that the semantics is given a priority in suggesting the pattern of reasoning and the abstractions of program behaviours. Moreover, as annotations can faithfully represent control flows of programs, no need for auxiliary variables arises. We consider also a method which allows us to isolate some inessential interleavings of concurrent actions and ignore them in correctness proofs, where a partial commutativity relation on actions is exploited. The concepts of trace theory provide a convenient framework for this study. Investigating this particular issue in an assertional framework was in fact an important objective from the outset of this work.