Proving Liveness Properties of Concurrent Programs

1982 ◽  
Vol 4 (3) ◽  
pp. 455-495 ◽  
Author(s):  
Susan Owicki ◽  
Leslie Lamport
Keyword(s):  
Concurrent Programs ◽  
Liveness Properties

scholarly journals Making weak memory models fair

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-27
Author(s):  
Ori Lahav ◽  
Egor Namakonov ◽  
Jonas Oberhauser ◽  
Anton Podkopaev ◽  
Viktor Vafeiadis
Keyword(s):  
Declarative Memory ◽  
Mutual Exclusion ◽  
Memory Models ◽  
Memory Model ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Formal Proofs ◽  
Liveness Properties ◽  
Uniform Definition ◽  
Fairness Condition

Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose a uniform definition for memory fairness that can be integrated into any declarative memory model enforcing acyclicity of the union of the program order and the reads-from relation. For the well-known models, SC, x86-TSO, RA, and StrongCOH, that have equivalent operational and declarative presentations, we show that our declarative memory fairness condition is equivalent to an intuitive model-specific operational notion of memory fairness, which requires the memory system to fairly execute its internal propagation steps. Our fairness condition preserves the correctness of local transformations and the compilation scheme from RC11 to x86-TSO, and also enables the first formal proofs of termination of mutual exclusion lock implementations under declarative weak memory models.

Causal-Consistent Replay Reversible Semantics for Message Passing Concurrent Programs

2021 ◽  
Vol 178 (3) ◽  
pp. 229-266
Author(s):  
Ivan Lanese ◽  
Adrián Palacios ◽  
Germán Vidal
Keyword(s):  
Programming Language ◽  
Message Passing ◽  
Concurrent Programming ◽  
Concurrent Systems ◽  
Concurrent Programs ◽  
Unified Framework ◽  
Innovative Technique ◽  
Dual Notion

Causal-consistent reversible debugging is an innovative technique for debugging concurrent systems. It allows one to go back in the execution focusing on the actions that most likely caused a visible misbehavior. When such an action is selected, the debugger undoes it, including all and only its consequences. This operation is called a causal-consistent rollback. In this way, the user can avoid being distracted by the actions of other, unrelated processes. In this work, we introduce its dual notion: causal-consistent replay. We allow the user to record an execution of a running program and, in contrast to traditional replay debuggers, to reproduce a visible misbehavior inside the debugger including all and only its causes. Furthermore, we present a unified framework that combines both causal-consistent replay and causal-consistent rollback. Although most of the ideas that we present are rather general, we focus on a popular functional and concurrent programming language based on message passing: Erlang.

scholarly journals Mechanized verification of fine-grained concurrent programs

2015 ◽  
Vol 50 (6) ◽  
pp. 77-87 ◽  
Author(s):  
Ilya Sergey ◽  
Aleksandar Nanevski ◽  
Anindya Banerjee
Keyword(s):  
Concurrent Programs ◽  
Fine Grained ◽  
Mechanized Verification

A generic approach to the static analysis of concurrent programs with procedures

2003 ◽  
Vol 38 (1) ◽  
pp. 62-73 ◽  
Author(s):  
Ahmed Bouajjani ◽  
Javier Esparza ◽  
Tayssir Touili
Keyword(s):  
Static Analysis ◽  
Concurrent Programs
Sign in / Sign up

Export Citation Format

Share Document