Axiomatic treatment of processes with shared variables revisited.

*(English)*Zbl 0748.68040Summary: The aim of this paper is to develop simple and practically useful formalisms for reasoning about processes with shared variables. Our approach is based on the axiomatic system described by N. Soundararajan [Theor. Comput. Sci. 31, 13-29 (1984; Zbl 0543.68010)]. In contrast to that work, our formalism is first derived from a model; this guarantees soundness and completeness of the formal proof system, with respect to the model. As an additional advantage the rules become simpler than those of Soundararajan; in particular, the local assertions may freely refer to shared variables; and we remove the explicit use of the compatibility predicate.

Next we augment the formalism by allowing global invariants, which may refer to shared variables (including shared histories), but with a different semantics than in the local assertions. The augmented system makes reasoning simpler in the sense that reasoning about the past is replaced by reasoning about the present. Finally we suggest a sufficiently complete set of mythical (auxiliary) variables free from embedded program structure. We demonstrate our formalism on some examples.

Next we augment the formalism by allowing global invariants, which may refer to shared variables (including shared histories), but with a different semantics than in the local assertions. The augmented system makes reasoning simpler in the sense that reasoning about the past is replaced by reasoning about the present. Finally we suggest a sufficiently complete set of mythical (auxiliary) variables free from embedded program structure. We demonstrate our formalism on some examples.

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

##### Keywords:

specification; verification; concurrency; reasoning about processes; shared variables; proof system
Full Text:
DOI

##### References:

[1] | Ashcroft, E.A.: Proving Assertions about Parallel Programs.Journal of Computer and System Sciences,10(1), 110-135 (1975). · Zbl 0299.68013 · doi:10.1016/S0022-0000(75)80018-3 |

[2] | Dahl, O.-J.: Time Sequences as a Tool for Describing Program Behaviour, Research Report 48, Department of Informatics, University of Oslo, Norway, 1979. |

[3] | Dahl, O.-J.: Parallel Programming (in Norwegian), Kompendium no. 46, Department of Informatics, University of Oslo, Norway, 1989. |

[4] | DÆhlin, J.H.: Semantikk om invarians og progresjon (Semantics for Safety and Liveness), Master Thesis (In Norwegian), Department of Informatics, University of Oslo, Norway, 1987. |

[5] | Gjessing, S. and Munthe-Kaas, E.: Trace Based Verification of Parallel Programs with Shared Variables 22nd Hawaii Int. Conf. on System Sciences, 3-6 January 1989. |

[6] | Hoare, C.A.R.: An Axiomatic Basis for Computer Programming,CACM,12(10), 576-583 (1969). · Zbl 0179.23105 |

[7] | Jones, C.B.: Specification and Design of (Parallel) Programs, Proc. IFIP 9th World Computer Congress, North Holland, pp. 321-332, 1983. |

[8] | Kahn, G.: The Semantics of a Simple Language for Parallel Programming, Information Processing 74, North-Holland, 1974. · Zbl 0299.68007 |

[9] | Lamport, L.: The ?Hoare Logic? of Concurrent Programs, Acta Informatica,14, 21-37 (1980). · Zbl 0428.68041 · doi:10.1007/BF00289062 |

[10] | Lamport, L.: Predicate Transformers for Concurrency, Technical Report, Digital System Center, CA, 1987 (Revised 1988). |

[11] | Manna, Z. and Pnueli, A.: Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.Science of Computer Programming,4(3) 257-289 (1984) (and STAN-CS-84-1005). · Zbl 0542.68014 · doi:10.1016/0167-6423(84)90003-0 |

[12] | Meldal, S.: On Hierarchical Abstraction and Partial Correctness of Concurrent Structures, Ph.D. thesis, Department of Informatics, University of Oslo, Norway, 1986 (also inBIT,26(2), 164-174 (1986)). · Zbl 0599.68029 |

[13] | Meldal, S.: Private communication. Department of Informatics, University of Bergen, Norway, 1989. |

[14] | Owicki, S. and Gries, D.: An Axiomatic Proof Technique for Parallel Programs.Acta Informatica,6 319-340 (1976). · Zbl 0324.68007 · doi:10.1007/BF00268134 |

[15] | Owicki, S. and Lamport, L.: Proving Liveness Properties of Concurrent Programs.ACM Transactions on Programming Languages and Systems,4(3) 455-495 (1982). · Zbl 0483.68013 · doi:10.1145/357172.357178 |

[16] | Soundararajan, N. and Dahl, O.-J.: Partial Correctness Semantics of Communicating Sequential Processes, Research Report 66, Department of Informatics, University of Oslo, Norway, 1982. |

[17] | Soundararajan, N.: A Proof Technique for Parallel Programs.Theoretical Computer Science,31, 13-29 (1984). · Zbl 0543.68010 · doi:10.1016/0304-3975(84)90122-1 |

[18] | Stirling, C.P.: A Generalization of Owicki-Gries’ Hoare Logic for a Concurrent While Language.Journal of Theoretical Computer Science,58, 347-360 (1988). · Zbl 0653.03017 · doi:10.1016/0304-3975(88)90033-3 |

[19] | StØlen, K.: Development of Parallel Programs on Shared Data-Structures, Ph.D. thesis, Manchester University, Manchester, UK, 1990. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.