Write a Blog >>
ICSE 2023
Sun 14 - Sat 20 May 2023 Melbourne, Australia
Wed 17 May 2023 13:45 - 14:00 at Meeting Room 110 - Program translation and synthesis Chair(s): Andy Zaidman

Concurrent programs suffer from data races. To prevent data races, programmers use locks. However, programs can eliminate data races only when they acquire and release correct locks at correct timing. The lock API of C, in which people have developed a large portion of legacy system programs, does not validate the correct use of locks. On the other hand, Rust, a recently developed system programming language, provides a lock API that guarantees the correct use of locks via type checking. This makes rewriting legacy system programs in Rust a promising way to retrofit safety into them. Unfortunately, manual C-to-Rust translation is extremely laborious due to the discrepancies between their lock APIs. Even the state-of-the-art automatic C-to-Rust translator retains the C lock API, expecting developers to replace them with the Rust lock API. In this work, we propose an automatic tool to replace the C lock API with the Rust lock API. It facilitates C-to-Rust translation of concurrent programs with less human effort than the current practice. Our tool consists of a Rust code transformer that takes a lock summary as an input and a static analyzer that efficiently generates precise lock summaries. We show that the transformer is scalable and widely applicable while preserving the semantics; it transforms 66 KLOC in 2.6 seconds and successfully handles 74% of real-world programs. We also show that the analyzer is scalable and precise; it analyzes 66 KLOC in 4.3 seconds.

Wed 17 May

Displayed time zone: Hobart change

13:45 - 15:15
Program translation and synthesisTechnical Track / Showcase / NIER - New Ideas and Emerging Results at Meeting Room 110
Chair(s): Andy Zaidman Delft University of Technology
13:45
15m
Talk
Concrat: An Automatic C-to-Rust Lock API Translator for Concurrent Programs
Technical Track
Pre-print
14:00
15m
Talk
Triggers for Reactive Synthesis Specifications
Technical Track
Gal Amram Tel Aviv University, Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University, Or Pistiner Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar
Pre-print
14:15
15m
Talk
Using Reactive Synthesis: An End-to-End Exploratory Case Study
Technical Track
Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University
Pre-print
14:30
15m
Talk
Pegasus: A Framework for Sound Continuous Invariant Generation
Showcase
Andrew Sogokon , Stefan Mitsch Carnegie Mellon University, USA, Yong Kiam Tan Carnegie Mellon University, Katherine Kosaian CMU, Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology (KIT)
14:45
7m
Talk
On ML-Based Program Translation: Perils and Promises
NIER - New Ideas and Emerging Results
Aniketh Malyala Yale University, Katelyn Zhou Silver Creek High School, Baishakhi Ray Columbia University, Saikat Chakraborty Microsoft Research
Pre-print
14:52
15m
Talk
Syntax and Domain Aware Model for Unsupervised Program Translation
Technical Track
Fang Liu Beihang University, Jia Li Peking University, Li Zhang Beihang University
Pre-print