6533b852fe1ef96bd12aad52
RESEARCH PRODUCT
Sequentializing Parameterized Programs
Gennaro ParlatoP. MadhusudanSalvatore La Torresubject
FOS: Computer and information sciencesComputer Science - Logic in Computer ScienceScheduleComputer scienceD.2.4;F.3.1Interface (computing)Parameterized complexitymodel-checking02 engineering and technologyThread (computing)computer.software_genrelcsh:QA75.5-76.95parameterized programsComputer Science - Software Engineeringsoftware verification0202 electrical engineering electronic engineering information engineeringBlock (data storage)Programming languagelcsh:MathematicsD.2.4Local variable020207 software engineeringlcsh:QA1-939Logic in Computer Science (cs.LO)Software Engineering (cs.SE)Transformation (function)model-checking; software verification; parameterized programs020201 artificial intelligence & image processinglcsh:Electronic computers. Computer scienceState (computer science)F.3.1computerdescription
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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2012-01-01 | Electronic Proceedings in Theoretical Computer Science |