Exposing Latent Mutual Exclusion by Work Automata - Topics in Theoretical Computer Science Access content directly
Conference Papers Year : 2017

Exposing Latent Mutual Exclusion by Work Automata

Kasper Dokter
  • Function : Author
  • PersonId : 1030366
Farhad Arbab
  • Function : Author
  • PersonId : 1007039


A concurrent application consists of a set of concurrently executing interacting processes. Although earlier we proposed work automata to specify both computation and interaction of such a set of executing processes, a detailed formal semantics for them was left implicit. In this paper, we provide a formal semantics for work automata, based on which we introduce equivalences such as weak simulation and weak language inclusion. Subsequently, we define operations on work automata that simplify them while preserving these equivalences. Where applicable, these operations simplify a work automaton by merging its different states into a state with a ‘more inclusive’ state-invariant. The resulting state-invariant defines a region in a multidimensional real vector space that potentially contains holes, which in turn expose mutual exclusion among processes. Such exposed dependencies provide additional insight in the behavior of an application, which can enhance scheduling. Our operations, therefore, potentially expose implicit dependencies among processes that otherwise may not be evident to exploit.
Fichier principal
Vignette du fichier
440117_1_En_6_Chapter.pdf (352.37 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01760644 , version 1 (06-04-2018)





Kasper Dokter, Farhad Arbab. Exposing Latent Mutual Exclusion by Work Automata. 2nd International Conference on Topics in Theoretical Computer Science (TTCS), Sep 2017, Tehran, Iran. pp.59-73, ⟨10.1007/978-3-319-68953-1_6⟩. ⟨hal-01760644⟩
42 View
34 Download



Gmail Facebook X LinkedIn More