Approaches to Shared State in Concurrent Programs

Program Verification with Separation Logic and Rely Guarantee

10.26686/wgtn.17060108 ◽

2021 ◽

Author(s):

◽

Allan Tabilog

Keyword(s):

Program Verification ◽

Separation Logic ◽

Concurrent Programs ◽

Abstract Data Type ◽

Data Abstraction ◽

Global State ◽

Shared Variable ◽

Concurrent Program ◽

Abstract Data ◽

Shared State

<p>This thesis explores two kinds of program logics that have become important for modern program verification - separation logic, for reasoning about programs that use pointers to build mutable data structures, and rely guarantee reasoning, for reasoning about shared variable concurrent programs. We look more closely into the motivations for merging these two kinds of logics into a single formalism that exploits the benefits of both approaches - local, modular, and explicit reasoning about interference between threads in a shared memory concurrent program. We discuss in detail two such formalisms - RGSep and Local Rely Guarantee (LRG), in particular we analyse how each formalism models program state and treats the distinction between global state (shared by all threads) and local state (private to a given thread) and how each logic models actions performed by threads on shared state, and look into the proof rules specifically for reasoning about atomic blocks of code. We present full examples of proofs in each logic and discuss their differences. This thesis also illustrates how a weakest precondition semantics for separation logic can be used to carry out calculational proofs. We also note how in essence these proofs are data abstraction proofs showing that a data structure implements some abstract data type, and relate this idea to a classic data abstraction technique by Hoare. Finally, as part of the thesis we also present a survey of tools that are currently available for doing manual or semi-automated proofs as well as program analyses with separation logic and rely guarantee.</p>

Download Full-text

Program Verification with Separation Logic and Rely Guarantee

10.26686/wgtn.17060108.v1 ◽

2021 ◽

Author(s):

◽

Allan Tabilog

Keyword(s):

Program Verification ◽

Separation Logic ◽

Concurrent Programs ◽

Abstract Data Type ◽

Data Abstraction ◽

Global State ◽

Shared Variable ◽

Concurrent Program ◽

Abstract Data ◽

Shared State

<p>This thesis explores two kinds of program logics that have become important for modern program verification - separation logic, for reasoning about programs that use pointers to build mutable data structures, and rely guarantee reasoning, for reasoning about shared variable concurrent programs. We look more closely into the motivations for merging these two kinds of logics into a single formalism that exploits the benefits of both approaches - local, modular, and explicit reasoning about interference between threads in a shared memory concurrent program. We discuss in detail two such formalisms - RGSep and Local Rely Guarantee (LRG), in particular we analyse how each formalism models program state and treats the distinction between global state (shared by all threads) and local state (private to a given thread) and how each logic models actions performed by threads on shared state, and look into the proof rules specifically for reasoning about atomic blocks of code. We present full examples of proofs in each logic and discuss their differences. This thesis also illustrates how a weakest precondition semantics for separation logic can be used to carry out calculational proofs. We also note how in essence these proofs are data abstraction proofs showing that a data structure implements some abstract data type, and relate this idea to a classic data abstraction technique by Hoare. Finally, as part of the thesis we also present a survey of tools that are currently available for doing manual or semi-automated proofs as well as program analyses with separation logic and rely guarantee.</p>

Download Full-text

Truly stateless, optimal dynamic partial order reduction

Proceedings of the ACM on Programming Languages ◽

10.1145/3498711 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-28

Author(s):

Michalis Kokologiannakis ◽

Iason Marmanis ◽

Vladimir Gladstein ◽

Viktor Vafeiadis

Keyword(s):

Partial Order ◽

Equivalence Class ◽

Order Reduction ◽

Concurrent Programs ◽

Partial Order Reduction ◽

Sequential Consistency ◽

Memory Consumption ◽

Optimal Dynamic ◽

Shared State ◽

Trace Equivalence

Dynamic partial order reduction (DPOR) verifies concurrent programs by exploring all their interleavings up to some equivalence relation, such as the Mazurkiewicz trace equivalence. Doing so involves a complex trade-off between space and time. Existing DPOR algorithms are either exploration-optimal (i.e., explore exactly only interleaving per equivalence class) but may use exponential memory in the size of the program, or maintain polynomial memory consumption but potentially explore exponentially many redundant interleavings. In this paper, we show that it is possible to have the best of both worlds: exploring exactly one interleaving per equivalence class with linear memory consumption. Our algorithm, TruSt, formalized in Coq, is applicable not only to sequential consistency, but also to any weak memory model that satisfies a few basic assumptions, including TSO, PSO, and RC11. In addition, TruSt is embarrassingly parallelizable: its different exploration options have no shared state, and can therefore be explored completely in parallel. Consequently, TruSt outperforms the state-of-the-art in terms of memory and/or time.

Download Full-text

Formal Specification and Verification of Concurrent Programs

10.21236/ada265201 ◽

1993 ◽

Cited By ~ 2

Author(s):

Daniel M. Berry

Keyword(s):

Formal Specification ◽

Concurrent Programs ◽

Formal Specification And Verification ◽

Specification And Verification

Download Full-text

Causal-Consistent Replay Reversible Semantics for Message Passing Concurrent Programs

Fundamenta Informaticae ◽

10.3233/fi-2021-2005 ◽

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.

Download Full-text