Wed 24 Mar 2021 18:30 - 19:00 at Virtual Space B - Session 6 Chair(s): Ademar Aguiar
Thu 25 Mar 2021 15:30 - 16:00 at Virtual Space B - Session 10 Chair(s): Mariana Marasoiu

This work strives to make formal verification of POSIX multithreaded programs easily accessible to general programmers. Sthread operates directly on multithreaded C/C++ programs, without the need for an intermediate formal model. Sthread is in-vivo in that it provides a drop-in replacement for the pthread library, and operates directly on the compiled target executable and application libraries. There is no compiler-generated intermediate representation. The system calls in the application remain unaltered. Optionally, the programmer can add a small amount of additional native C code to include assertions based on the user’s algorithm, declarations of shared memory regions, and progress/liveness conditions. The work has two important motivations: (i) It can be used to verify correctness of a concurrent algorithm being implemented with multithreading; and (ii) it can also be used pedagogically to provide immediate feedback to students learning either to employ POSIX threads system calls or to implement multithreaded algorithms.

This work represents the first example of in-vivo model checking operating directly on the standard multithreaded executable and its libraries, without the aid of a compiler-generated intermediate representation. Sthread leverages the open-source SimGrid libraries, and will eventually be integrated into SimGrid. Sthread employs a non-preemptive model in which thread context switches occur only at multithreaded system calls (e.g., mutex, semaphore) or before accesses to shared memory regions. The emphasis is on finding “algorithmic bugs” (bugs in an original algorithm, implemented as POSIX threads and shared memory regions. This work is in contrast to Context-Bounded Analysis (CBA), which assumes a preemptive model for threads, and emphasizes implementation bugs such as buffer overruns and write-after-free for memory allocation. In particular, the Sthread in-vivo approach has strong future potential for pedagogy, by providing immediate feedback to students who are first learning the correct use of Pthreads system calls in implementation of concurrent algorithms based on multithreading.

Conference Day
Wed 24 Mar

Displayed time zone: Belfast change

17:30 - 19:00
Session 6Research Papers at Virtual Space B
Chair(s): Ademar AguiarFEUP, Universidade do Porto
17:30
30m
Live Q&A
Constructing Hybrid Incremental Compilers for Cross-Module Extensibility with an Internal Build System
Research Papers
Jeff SmitsDelft University of Technology, Netherlands, Gabriël KonatDelft University of Technology, Eelco VisserDelft University of Technology
DOI Media Attached
18:00
30m
Live Q&A
Functional Programming in Pattern-Match-Oriented Programming Style
Research Papers
Satoshi EgiRakuten Institute of Technology, Rakuten, Inc. / The University of Tokyo, Yuichi NishiwakiThe University of Tokyo
DOI Media Attached
18:30
30m
Live Q&A
Sthread: In-Vivo Model Checking of Multithreaded Programs
Research Papers
Gene CoopermanNortheastern University, Martin QuinsonÉcole Normale Supérieure Rennes
DOI Media Attached

Conference Day
Thu 25 Mar

Displayed time zone: Belfast change

15:00 - 16:30
Session 10Research Papers at Virtual Space B
Chair(s): Mariana MarasoiuUniversity of Cambridge
15:00
30m
Live Q&A
Constructing Hybrid Incremental Compilers for Cross-Module Extensibility with an Internal Build System
Research Papers
Jeff SmitsDelft University of Technology, Netherlands, Gabriël KonatDelft University of Technology, Eelco VisserDelft University of Technology
DOI Media Attached
15:30
30m
Live Q&A
Sthread: In-Vivo Model Checking of Multithreaded Programs
Research Papers
Gene CoopermanNortheastern University, Martin QuinsonÉcole Normale Supérieure Rennes
DOI Media Attached