Write a Blog >>
Fri 24 Jan 2020 11:13 - 11:35 at Ile de France II (IDF II) - Type Systems Chair(s): Dominique Devriese

We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a type system that checks whether a program properly manages its memory. If the type check succeeds, it is safe to ignore the SMR algorithm and consider the program under garbage collection. Intuitively, our types track the protection of pointers as guaranteed by the SMR algorithm. There are two design decisions. The type system does not track any shape information, which makes it extremely lightweight. Instead, we rely on invariant annotations that postulate a protection by the SMR. To this end, we introduce angels, ghost variables with an angelic semantics. Moreover, the SMR algorithm is not hard-coded but a parameter of the type system definition. To achieve this, we rely on a recent specification language for SMR algorithms. Our second contribution is to automate the type inference and the invariant check. For the type inference, we show a quadratic-time algorithm. For the invariant check, we give a source-to-source translation that links our programs to off-the-shelf verification tools. It compiles away the angelic semantics. This allows us to infer appropriate annotations automatically in a guess-and-check manner. To demonstrate the effectiveness of our type-based verification approach, we check linearizability for various list and set implementations from the literature with both hazard pointers and epoch-based memory reclamation. For many of the examples, this is the first time they are verified automatically. For the ones where there is a competitor, we obtain a speed-up of up to two orders of magnitude.

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Type SystemsResearch Papers at Ile de France II (IDF II)
Chair(s): Dominique Devriese Vrije Universiteit Brussel
10:30
21m
Talk
Kind Inference for DatatypesDistinguished Paper
Research Papers
Ningning Xie University of Toronto, Richard A. Eisenberg Bryn Mawr College, USA, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong
Link to publication DOI Media Attached
10:51
21m
Talk
Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Research Papers
Mark Jones Portland State University, J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Research Papers
Roland Meyer TU Braunschweig, Sebastian Wolff TU Braunschweig
Link to publication DOI Media Attached File Attached