参数化程序的序列化
Sequentializing Parameterized Programs
摘要：
我们表现出断言保持（可达性保持）的参数化并发共享内存程序的转换，在一个k轮调度的进程，顺序程序。顺序程序的显著特点是它在任何时候只跟踪一个线程的局部变量，并且只使用O（k）个共享变量的副本（它不使用额外的计数器，甚至不使用一个计数器来跟踪线程的数量）。序列化是使用线性接口的概念来实现的，该线性接口捕获了无界进程块对k轮调度中的共享状态的影响。我们的转换利用线性接口来序列化程序，并确保序列程序只探索可达状态并保留局部不变量。
英文摘要：
We exhibit assertion-preserving (reachability preserving) transformations from parameterized concurrent shared-memory programs, under a k-round scheduling of processes, to sequential programs. The salient feature of the sequential program is that it tracks the local variables of only one thread at any point, and uses only O(k) copies of shared variables (it does not use extra counters, not even one counter to keep track of the number of threads). Sequentialization is achieved using the concept of a linear interface that captures the effect an unbounded block of processes have on the shared state in a k-round schedule. Our transformation utilizes linear interfaces to sequentialize the program, and to ensure the sequential program explores only reachable states and preserves local invariants.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
