PhD Courses in Programming Languages

Software maintained by members of the group

Tools for Analysis, Testing and Verification of Erlang Programs

• Concuerror: A stateless model checking tool for systematically exploring all process interleaving of an Erlang program.
• Dialyzer: A static analysis tool that automatically detects discrepancies (many of which are bugs) in Erlang programs.

Locking Libraries

• Queue Delegation Locking: C and C++ libraries for QD Locking.

Concurrent Data Structures

• Contention Adapting Binary Search Trees: offering Java and C implementations.
• Contention Avoiding Priority Queue: offering C implementation.

Concuerror is a systematic testing (aka, stateless model checking) tool for finding and reproducing concurrency errors in Erlang programs.

You can more find information about Concuerror (its code, tutorials, relevant publications, etc.) on its dedicated website: http://parapluu.github.io/Concuerror

People maintaining Concuerror:

• Stavros Aronis
• Kostis Sagonas

Since 2014, Concuerror's development has been partly supported by UPMARC and the EU project RELEASE.

This page contains information for Dialyzer, the DIscrepancy AnaLYZer for ERlang applications.

OVERVIEW

Dialyzer is a static analysis tool that identifies software discrepancies such as definite type errors, code which has become dead or unreachable due to some programming error, unnecessary tests, etc. in single Erlang modules or entire (sets of) applications. Dialyzer starts its analysis from either debug-compiled BEAM bytecode or from Erlang source code. The file and line number of a discrepancy is reported along with an indication of what the discrepancy is about. Dialyzer bases its analysis on the concept of success typings which allows for sound warnings (no false positives).

DOWNLOAD

Since 2007, Dialyzer is included in the official Erlang/OTP distribution.

RESOURCES

You can find more information on how to use Dialyzer here.

PEOPLE

The first versions of Dialyzer were created by Tobias Lindahl and Kostis Sagonas.

People actively working and maintaining Dialyzer are Stavros Aronis and Kostis Sagonas.

People who have also worked on improvements of Dialyzer in the past are Maria Christakis, Elli Fragkaki and Ypatia Tsavliri.

Queue Delegation (QD) Locking is an efficient delegation technique for synchronization in multi-threaded programs. QD locking significantly outperforms traditional locking libraries (e.g., pthreads locks) and performs better than delegation mechanisms that have been proposed in the literature. An advantage of all delegation algorithms is that the lock holding thread can execute many critical sections in sequence while it has the data protected by the critical section in its fast private cache. In most applications, QD locks can be used as a drop-in replacement of traditional locks, by delegating the critical operation and waiting for its result. However, QD locks also offer threads the possibility to do detached execution: i.e., for threads to delegate their critical sections to the current lock holder and continue their execution without waiting for the result of the delegated operation. Of course, to get the benefits of detached execution, our QD locking libraries also provide a lock interface which differs from that provided by traditional locks.

The idea, algorithms and properties of QD locking as well as extensive comparisons with similar algorithms can be found in an article in the IEEE Transactions on Parallel and Distributed Systems journal. An unedited pre-print version of that article can also found in the list of publications below. The main idea of QD locking has also been described in a SPAA'2014 brief announcement. The interface of the queue delegation libraries we provide as well as experiences from using them in code bases of significant size are described in a paper that has been published in the proceedings of EuroPar'2014. See the list of publications below for more information about the publications.

PUBLICATIONS

• David Klaftenegger, Konstantinos Sagonas, and Kjell Winblad. Queue Delegation Locking. In IEEE Transactions on Parallel and Distributed Systems. 2017. [BibTeX citation]

• David Klaftenegger, Konstantinos Sagonas, and Kjell Winblad. Brief Announcement: Queue Delegation Locking. In Proceedings of the 26th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 70-72, June 2014. ACM Press. [BibTeX citation]

• David Klaftenegger, Konstantinos Sagonas, and Kjell Winblad. Delegation Locking Libraries for Improved Performance of Multithreaded Programs In Euro-Par 2014, Proceedings of the 20th International Conference, pp. 572-583, Volume 8632 in LNCS, August 2014. Springer. [BibTeX citation]

LIBRARIES FOR C AND C++

• Library for C The QD locking library for C is a complete locking library designed with QD locking in mind. This tutorial is a good introduction to the API of the library. More information can be found on the library's website.

• Library for C++ This github repository contains the header files needed for a C++ version of QD locking. It differs from the C version in its more accessible interface that makes it easier to use in C++ code, while also providing type safety.

AUTOMATIC CODE TRANSFORMATION

This tool can be used to automatically transform C source code that use pthread mutex locks to instead use QD locks from the C library above.

The tool is still a prototype, but can already be used for code bases of limited complexity. The tool has been developed by Robert Markovski as his bachelor thesis project.

BENCHMARKS

• Benchmarking for Queue Delegation Locks This github repository contains benchmarking code that we used to evaluate QD locking. The necessary locking code is included in this repository, so neither of the libraries needs to be downloaded together with this.

A contention adapting search tree is a concurrent ordered set data structure that adapts its synchronization granularity according to the contention level. We have described two types of contention adapting search trees. One of them is lock-based and one is lock-free. This page contains links to contention adapting search tree related papers, implementations, benchmarks and performance graphs.

PUBLICATIONS

The lock-free contention adapting search tree (LFCA tree) is described in the following publications:

• Kjell Winblad, Bengt Jonsson and Konstantinos Sagonas. Lock-free Contention Adapting Search Trees. ACM Transactions on Parallel Computing, Volume 8, Issue 2, Article No. 10, pages 1–38, June 2021. (publisher's version).

• Kjell Winblad, Bengt Jonsson and Konstantinos Sagonas. Lock-free Contention Adapting Search Trees. 30th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA 2018). (see note here, publisher's version, preprint, code)

A comprehensive description of the lock-based contention adapting search tree (CA tree) with support for the operations insert, delete, lookup and range query is given in the journal publication below. This publication contains a detailed description of the data structure including pseudo-code and proofs for the correctness properties (linearizability, deadlock freedom and livelock freedom).

• Konstantinos Sagonas and Kjell Winblad. A contention adapting approach to concurrent ordered sets. Journal of Parallel and Distributed Computing, 2018 (submitted 2016). (publisher's version, preprint, code)

The journal publication above is built upon the following two conference publications. The first of those papers describes CA trees with support for single-element operations (insert, delete, and lookup). This paper contains two experimental evaluations of CA tree optimizations that are not included in the journal paper above. One of these optimzations is for use cases with very high contention. The other one combines a CA tree with hardware lock elision. The second paper evaluates and describes a CA tree extension to support linearizable range operations (range queries and range updates) and bulk operations. The technical report that is referred to in these two papers has been replaced by the journal publication above.

• Konstantinos Sagonas and Kjell Winblad. Contention Adapting Search Trees. In Proceedings of the Fourteenth International Symposium on Parallel and Distributed Computing, Limassol, Cyprus, July 2015. (publisher's version, preprint, code)
• Konstantinos Sagonas and Kjell Winblad. Efficient Support for Range Queries and Range Updates Using Contention Adapting Search Trees. In Proceedings of the 28th International Workshop on Languages and Compilers for Parallel Computing, Raleigh, USA, September 2015. (publisher's version, preprint, code)

The publication below describes an optimization for CA trees that is enabled by using an immutable data structure internally. This optimization is especially beneficial for range queries when contention is high. The experimental results presented in the paper show that the optimized CA tree variant outperform many recently proposed data structures in many scenarios. The benchmark code and the code for the optimized CA tree variant is available here.

• Kjell Winblad. Faster Concurrent Range Queries with Contention Adapting Search Trees Using Immutable Data. In the proceedings of 2017 Imperial College Computing Student Workshop (ICCSW 2017), London, United Kingdom, September 2017. (publisher's version, preprint, code)

The publication below describes how CA trees can be used to improve the scalability of the Erlang Term Storage.

• Konstantinos Sagonas and Kjell Winblad. More Scalable Ordered Set for ETS Using Adaptation. In Proceedings of the Thirteenth ACM SIGPLAN Workshop on Erlang, pages 3-11, Gothenburg, Sweden, September 2014.

BENCHMARKS AND CODE

The code used to obtain the experimental results included in the CA tree papers can be found by following the links with the text "code" that can be found next to the citations above.

Efficient and scalable concurrent priority queues are crucial for the performance of many multicore applications, e.g. for task scheduling and the parallelization of various algorithms. Linearizable concurrent priority queues with traditional semantics suffer from an inherent sequential bottleneck in the head the queue. This bottleneck is the motivation for some recently proposed priority queues with more relaxed semantics. We present the contention avoiding concurrent priority queue (CA-PQ), a data structure that functions as a linearizable concurrent priority with traditional semantics under low contention, but activates contention avoiding techniques that give it more relaxed semantics when high contention is detected. CA-PQ avoids contention in the head of the queue by removing items in bulk from the global data structure, which also allows it to often serve DelMin operations without accessing memory that is modified by several threads. We show that CA-PQ scales well. Its cache friendly design achieves performance that is twice as fast compared to using state-of-the-art concurrent priority queues on several instances of a parallel shortest path benchmark.

PUBLICATIONS

• Konstantinos Sagonas and Kjell Winblad. The Contention Avoiding Concurrent Priority Queue In Languages and Compilers for Parallel Computing - 29th International Workshop (LCPC 2016), Revised papers, pages 314-330, Volume 10136 in LNCS, Rochester, NY, USA, September 2016. Springer.

An authors pre-print containing an additional appendix with more benchmark results is also available here:
The Contention Avoiding Concurrent Priority Queue.

CODE

• The code for the benchmark that is used in the paper.
• A cleaned up version of the CA-PQ code and the single source shortest path benchmark that is used in the paper has been included in the KLSM benchmark repository.