2026-07-21T19:38:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18256 2024-03-06T11:05:20Z ddc:004 open_access

ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs (Artifact) Suchert, Felix Zeidler, Lisza Castrillon, Jeronimo Ertel, Sebastian concurrent programming verification scalability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Felix Suchert and Lisza Zeidler and Jeronimo Castrillon and Sebastian Ertel 2023 Is Part Of DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.9.2.16 urn:nbn:de:0030-drops-182562 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.16 eng https://creativecommons.org/licenses/by/4.0/legalcode