Synchronised Shared Memory and Model Checking

Joaquín Aguado and Alejandra Duenas
Additional contact information
Joaquín Aguado: Otto-Friedrich-Universität Bamberg

Post-Print from HAL

Abstract: In this paper, a formal generic framework for defining and reasoning about deterministic concurrency in synchronous systems is implemented in the Spin model checker. Concretely, the paper implements the clock-synchronised shared memory ( csm ) theory , which extends synchronous programming with more and higher level csm data types. These csm data types are equipped with a synchronisation policy prescribing how concurrent calls to objects methods must be organised. In a policy constructive system, all methods of every object can be scheduled in a policy-conformant manner without deadlocking. In our framework, synchronous policies get codified as Promela never-claims. In this form, the model checker can search for executions (interleavings) that satisfy the synchronous product of all the never-claims, namely policy-conformant schedules for all the csm objects. The existence of such a policy-conformant schedules, verifies that the concurrent synchronous system is deterministic. The approach of this paper extends beyond a single semantics since it can handle the synchronous programming model as well as the various forms of the sequentially constructive model found in the literature.

Date: 2023-10-02
References: Add references at CitEc
Citations:

Published in ACM Transactions on Embedded Computing Systems (TECS), 2023, pp.1-30. ⟨10.1145/3626188⟩

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hal:journl:hal-04400956

DOI: 10.1145/3626188

Access Statistics for this paper

More papers in Post-Print from HAL
Bibliographic data for series maintained by CCSD ().