ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs (Artifact)

Authors Felix Suchert , Lisza Zeidler, Jeronimo Castrillon , Sebastian Ertel

Thumbnail PDF

Artifact Description

  • Filesize: 0.53 MB
  • 3 pages

Document Identifiers

Author Details

Felix Suchert
  • TU Dresden, Germany
Lisza Zeidler
  • Barkhausen Insitut, Dresden, Germany
Jeronimo Castrillon
  • TU Dresden, Germany
Sebastian Ertel
  • Barkhausen Institut, Dresden, Germany

Cite AsGet BibTex

Felix Suchert, Lisza Zeidler, Jeronimo Castrillon, and Sebastian Ertel. ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy


SAT/SMT-solvers and model checkers automate formal verification of sequential programs. Formal reasoning about scalable concurrent programs is still manual and requires expert knowledge. But scalability is a fundamental requirement of current and future programs. Sequential imperative programs compose statements, function/method calls and control flow constructs. Concurrent programming models provide constructs for concurrent composition. Concurrency abstractions such as threads and synchronization primitives such as locks compose the individual parts of a concurrent program that are meant to execute in parallel. We propose to rather compose the individual parts again using sequential composition and compile this sequential composition into a concurrent one. The developer can use existing tools to formally verify the sequential program while the translated concurrent program provides the dearly requested scalability. Following this insight, we present ConDRust, a new programming model and compiler for Rust programs. The ConDRust compiler translates sequential composition into a concurrent composition based on threads and message-passing channels. During compilation, the compiler preserves the semantics of the sequential program along with much desired properties such as determinism. Our evaluation shows that our ConDRust compiler generates concurrent deterministic code that can outperform even non-deterministic programs by up to a factor of three for irregular algorithms that are particularly hard to parallelize.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
  • Software and its engineering → Parallel programming languages
  • concurrent programming
  • verification
  • scalability


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Christian Bienia and Kai Li. Parsec 2.0: A new benchmark suite for chip-multiprocessors. In Proceedings of the 5th Annual Workshop on Modeling, Benchmarking and Simulation, volume 2011, page 37, 2009. Google Scholar
  2. Brian F. Cooper, Adam Silberstein, Erwin Tam, Raghu Ramakrishnan, and Russell Sears. Benchmarking cloud serving systems with ycsb. In Proceedings of the 1st ACM symposium on Cloud computing, pages 143-154, 2010. Google Scholar
  3. Chi Cao Minh, JaeWoong Chung, Christos Kozyrakis, and Kunle Olukotun. Stamp: Stanford transactional applications for multi-processing. In 2008 IEEE International Symposium on Workload Characterization, pages 35-46. IEEE, 2008. Google Scholar