论文标题
sthread：多线程程序的体内模型检查
Sthread: In-Vivo Model Checking of Multithreaded Programs
论文作者
论文摘要
这项工作旨在正式验证普通程序员可以轻松访问的POSIX多线程程序。 STHREAD直接在多线程C/C ++程序上运行，而无需中间正式模型。 STHREAD在体内，因为它为Pthread库提供了一个置换式替换，并直接在编译的目标可执行文件和应用程序库上运行。 没有编译器生成的中间表示。应用程序中的系统调用尚未改变。可选地，程序员可以添加少量的其他本机C代码，以包括基于用户算法，共享内存区域的声明以及进度/LINICICES条件的主张。 这项工作有两个重要的动机：（i）可以用来验证通过多线程实现的并发算法的正确性； （ii）它也可以在教学上使用，以向学习使用POSIX线程系统调用或实施多线程算法的学生提供即时反馈。 这项工作代表了直接在标准的多线程可执行文件及其库上操作的Vivo In-Vivo模型的第一个示例，而无需编译器生成的中间表示。 STHREAD利用开源Simgrid库，最终将集成到Simgrid中。 STHREAD采用了一个非抢先模型，其中线程上下文开关仅在多线程系统调用（例如Mutex，Smahaphore）或访问共享内存区域之前发生。 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教学法，通过向首先学习正确使用Pthreads系统调用的学生立即提供反馈，以实现基于多线程的并发算法。
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.
