We propose a general framework for compositional underapproximate concurrent program analyses by reduction to sequential program analyses-so-called sequentializations. We notice the existing sequentializations-based on bounding the number of execution contexts, execution rounds, or delays from a deterministic task-schedule-rely on three key features for scalable concurrent program analyses: (i) reduction to the sequential program model, (ii) compositional reasoning to avoid expensive task-product constructions, and (iii) parameterized exploration bounds. To understand how those sequentializations can be unified and generalized, we define a general framework which preserves their key features, and in which those sequentializations are particular instances. We also identify a most general instance which considers more executions, by composing the rounds of different tasks in any order, restricted only by the unavoidable program and task-creation causality orders. In fact, we show this general instance is fundamentally more powerful by identifying an infinite family of state-reachability problems (to states g1, g2,...) which can be answered precisely with a fixed exploration bound, whereas the existing sequentializations require an increasing bound k to reach each gk. Our framework applies to a general class of shared-memory concurrent programs, with dynamic task-creation and arbitrary preemption.

On Sequentializing Concurrent Programs

PARLATO G
2011-01-01

Abstract

We propose a general framework for compositional underapproximate concurrent program analyses by reduction to sequential program analyses-so-called sequentializations. We notice the existing sequentializations-based on bounding the number of execution contexts, execution rounds, or delays from a deterministic task-schedule-rely on three key features for scalable concurrent program analyses: (i) reduction to the sequential program model, (ii) compositional reasoning to avoid expensive task-product constructions, and (iii) parameterized exploration bounds. To understand how those sequentializations can be unified and generalized, we define a general framework which preserves their key features, and in which those sequentializations are particular instances. We also identify a most general instance which considers more executions, by composing the rounds of different tasks in any order, restricted only by the unavoidable program and task-creation causality orders. In fact, we show this general instance is fundamentally more powerful by identifying an infinite family of state-reachability problems (to states g1, g2,...) which can be answered precisely with a fixed exploration bound, whereas the existing sequentializations require an increasing bound k to reach each gk. Our framework applies to a general class of shared-memory concurrent programs, with dynamic task-creation and arbitrary preemption.
2011
978-3-642-23701-0
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11695/88418
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 28
  • ???jsp.display-item.citation.isi??? 19
social impact