ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs
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.
Wed 19 JulDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00
|Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types|
Sung-Shik Jongmans Open University of the Netherlands; CWI, Francisco Ferreira Royal Holloway, University of LondonDOI
|Asynchronous Multiparty Session Type Implementability is Decidable – Lessons Learned from Message Sequence Charts|
Felix Stutz MPI-SWSDOI
|Dynamically Updatable Multiparty Session Protocols|
|Designing Asynchronous Multiparty Protocols with Crash-Stop Failures|
Adam D. Barwell University of St Andrews and University of Oxford, Ping Hou University of Oxford, Nobuko Yoshida University of Oxford, Fangyi Zhou Imperial College LondonDOI Pre-print
|ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs|
Felix Suchert Center for Advancing Electronics Dresden, TU Dresden, Lisza Zeidler Composable Operating Systems Group, Barkhausen Institute, Dresden, Jeronimo Castrillon TU Dresden, Germany, Sebastian Ertel Composable Operating Systems Group, Barkhausen Institute, DresdenDOI
|Information Flow Analysis for Detecting Non-Determinism in Blockchain|
Luca Olivieri Ca’ Foscari University of Venice, Vincenzo Arceri University of Parma, Italy, Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Fabio Tagliaferro CYS4 Srl, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia, Fausto Spoto U. VeronaDOI