Simuliris: a separation logic framework for verifying concurrent program optimizations

Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of concurrent programs is to assume that the source program has no data races : if it does, they cause the program to have undefined behavior (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them). In this work we present Simuliris , the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using ownership to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of concurrent separation logics to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform thread-local proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.

Download Full-text

Compiling with continuations, correctly

Proceedings of the ACM on Programming Languages ◽

10.1145/3485491 ◽

2021 ◽

Vol 5 (OOPSLA) ◽

pp. 1-29

Author(s):

Zoe Paraskevopoulou ◽

Anvay Grover

Keyword(s):

Target Language ◽

Logical Relation ◽

Program Transformations ◽

Small Step ◽

Source Language ◽

Separate Compilation ◽

Source Program ◽

Coq Proof Assistant ◽

Semantic Correctness ◽

Simulation Relation

In this paper we present a novel simulation relation for proving correctness of program transformations that combines syntactic simulations and logical relations. In particular, we establish a new kind of simulation diagram that uses a small-step or big-step semantics in the source language and an untyped, step-indexed logical relation in the target language. Our technique provides a practical solution for proving semantics preservation for transformations that do not preserve reductions in the source language. This is common when transformations generate new binder names, and hence α-conversion must be explicitly accounted for, or when transformations introduce administrative redexes. Our technique does not require reductions in the source language to correspond directly to reductions in the target language. Instead, we enforce a weaker notion of semantic preorder, which suffices to show that semantics are preserved for both whole-program and separate compilation. Because our logical relation is transitive, we can transition between intermediate program states in a small-step fashion and hence the shape of the proof resembles that of a simple small-step simulation. We use this technique to revisit the semantic correctness of a continuation-passing style (CPS) transformation and we demonstrate how it allows us to overcome well-known complications of this proof related to α-conversion and administrative reductions. In addition, by using a logical relation that is indexed by invariants that relate the resource consumption of two programs, we are able show that the transformation preserves diverging behaviors and that our CPS transformation asymptotically preserves the running time of the source program. Our results are formalized in the Coq proof assistant. Our continuation-passing style transformation is part of the CertiCoq compiler for Gallina, the specification language of Coq.

Download Full-text

Linear capabilities for fully abstract compilation of separation-logic-verified code

Journal of Functional Programming ◽

10.1017/s0956796821000022 ◽

2021 ◽

Vol 31 ◽

Author(s):

THOMAS VAN STRYDONCK ◽

FRANK PIESSENS ◽

DOMINIQUE DEVRIESE

Keyword(s):

Spatial Separation ◽

Separation Logic ◽

Target Language ◽

Fine Grained ◽

Dynamic Contract ◽

Modular Verification ◽

Source Program ◽

Memory Accesses ◽

Memory Resources ◽

Efficient Memory

Abstract Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module. This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied. We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program. The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well. This article is an extended version of one that was presented at ICFP 2019 (Van Strydonck et al., 2019).

Download Full-text

Data races vs. data race bugs

ACM SIGARCH Computer Architecture News ◽

10.1145/2189750.2150997 ◽

2012 ◽

Vol 40 (1) ◽

pp. 185-198 ◽

Cited By ~ 8

Author(s):

Baris Kasikci ◽

Cristian Zamfir ◽

George Candea

Keyword(s):

Data Race ◽

Data Races

Download Full-text

Gobra: Modular Specification and Verification of Go Programs

Computer Aided Verification - Lecture Notes in Computer Science ◽

10.1007/978-3-030-81685-8_17 ◽

2021 ◽

pp. 367-379

Author(s):

Felix A. Wolf ◽

Linard Arquint ◽

Martin Clochard ◽

Wytse Oortwijn ◽

João C. Pereira ◽

...

Keyword(s):

Distributed Systems ◽

Programming Language ◽

Message Passing ◽

Safety Data ◽

Separation Logic ◽

Data Race ◽

Static Verification ◽

Crash Safety ◽

Concurrent And Distributed Systems ◽

Systems Programming

AbstractGo is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives.We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.

Download Full-text

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

Race Condition Detection Algorithms

International Journal of Engineering and Advanced Technology - Regular Issue ◽

10.35940/ijeat.b2696.129219 ◽

2019 ◽

Vol 9 (2) ◽

pp. 1242-1246

Keyword(s):

Programming Model ◽

Application Programming Interface ◽

Data Race ◽

Variable Environment ◽

Software Application ◽

Work Sharing ◽

Multiple Data ◽

Race Condition ◽

Multiple Threads ◽

Data Races

A data race is similar to any other bugs in software application. Data race will result in the execution of the program unpredictable. There are 46 documented races in Linux kernel. OpenMP is an Application programming interface for shared programming model. It is a construct based model which works on fork join parallelism. OpenMP achieved node level parallelism and can manage data in single instruction multiple data and single program multiple data parallelism by executing different constructs like work sharing and parallel constructs. In any shared programming model, variables are shared by multiple threads in the program to execute different tasks by different threads. OpenMP is used to achieve parallelism by creating shared variable environment but there are chances to have data races in OpenMP programs. In this paper we discuss different algorithms to detect data races in OpenMP programs.

Download Full-text

On incorrectness logic and Kleene algebra with top and tests

Proceedings of the ACM on Programming Languages ◽

10.1145/3498690 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-30

Author(s):

Cheng Zhang ◽

Arthur Azevedo de Amorim ◽

Marco Gaboardi

Keyword(s):

Equational Theory ◽

Program Transformations ◽

Hoare Logic ◽

Compiler Optimizations ◽

Partial Correctness ◽

Seminal Work ◽

Kleene Algebra

Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.

Download Full-text

Applying Program Transformations for Deductive Verification of the List Reverse Program

PROGRAMMNAYA INGENERIA ◽

10.17587/prin.12.127-139 ◽

2021 ◽

Vol 12 (3) ◽

pp. 127-139

Author(s):

V. I. Shelekhov ◽

Keyword(s):

Program Transformations ◽

Data Types ◽

Deductive Verification ◽

C Language ◽

Recursive Program ◽

Smt Solvers ◽

Source Program ◽

Predicate Language ◽

Transformation Methods ◽

Recursive Data

The program transformation methods to simplify the deductive verification of programs with recursive data types are investigated. The list reversion program is considered as an example. A source program in the C language is translated to the cP functional language which includes no pointers. The resulting program is translated further to the WhyML language to perform deductive verification of the program. The cP language includes the same constructs of the C language except pointers. In the C program, all actions that include pointers are replaced by the equivalent fragments without pointers. These replacement are performed by the special transformations using the results of the program dataflow analysis. Three variants of deductive verification of the transformed list reverse program in the Why3 verification platform with SMT solvers (Z3 4.8.6, CVC3 2.4.1, CVC4 1.7) are performed. First, the recursive WhyML program supplied with specifications was automatically verified successfully using only SMT solvers. Second, the recursive program was translated to the P predicate language. Correctness formulae were constructed for the P program and translated further to the why3 specification language. The formulae proving correctness were easy like the first variant. But correctness formulae for the first and second variants were different. Third, the "imperative" WhyML program that included while loop with additional invariant specifications was verified. The proving was easy but not automatic. So, for deductive verification, recursive program variant appears to be more preferable against imperative program variant.

Download Full-text