MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution)
MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution)
复制标题
DOI：
10.1007/978-3-642-54862-8_30
复制
发表时间：
2014-04
期刊：
影响因子：
--
通讯作者：
Ermenegildo Tomasco;Omar Inverso;B. Fischer;S. L. Torre;G. Parlato
中科院分区：
文献类型：
--
作者：
Ermenegildo Tomasco;Omar Inverso;B. Fischer;S. L. Torre;G. Parlato
我们实现了一个新的顺序化算法的多线程C程序与动态线程创建作为一个新的CSeq模块。该算法的基本思想是（通过不确定性猜测）固定共享内存中的写操作序列，然后根据尊重此选择的任何调度来模拟程序的行为。模拟是逐线程进行的，线程创建机制被函数调用取代。
We implement a new sequentialization algorithm for multi-threaded C programs with dynamic thread creation as a new CSeq module. The novel basic idea of this algorithm is to fix (by a nondeterministic guess) the sequence of write operations in the shared memory and then simulate the behavior of the program according to any scheduling that respects this choice. Simulation is done thread-by-thread and the thread creation mechanism is replaced by function calls.