Sequentializing parameterized programs

Salvatore La Torre, P. Madhusudan, Gennaro Parlato

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish (US)
Pages (from-to)48-55
Number of pages8
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume87
DOIs
StatePublished - Jul 15 2012
Event4th Workshop on Foundations of Interface Technologies, FIT 2012 - Tallinn, Estonia
Duration: Mar 25 2012 → …

Fingerprint

Linear transformations
Scheduling
Data storage equipment

ASJC Scopus subject areas

  • Software

Cite this

Sequentializing parameterized programs. / Torre, Salvatore La; Madhusudan, P.; Parlato, Gennaro.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 87, 15.07.2012, p. 48-55.

Research output: Contribution to journalConference article

@article{7527c4bd298f45f38893a75ded7166c3,
title = "Sequentializing parameterized programs",
abstract = "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.",
author = "Torre, {Salvatore La} and P. Madhusudan and Gennaro Parlato",
year = "2012",
month = "7",
day = "15",
doi = "10.4204/EPTCS.87.4",
language = "English (US)",
volume = "87",
pages = "48--55",
journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Sequentializing parameterized programs

AU - Torre, Salvatore La

AU - Madhusudan, P.

AU - Parlato, Gennaro

PY - 2012/7/15

Y1 - 2012/7/15

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85026634221&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85026634221&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.87.4

DO - 10.4204/EPTCS.87.4

M3 - Conference article

AN - SCOPUS:85026634221

VL - 87

SP - 48

EP - 55

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

SN - 2075-2180

ER -