Panini: A Concurrent Programming Model for Solving Pervasive and Oblivious Interference

By: Mehdi Bagherzadeh and Hridesh Rajan

Abstract

Modular reasoning about concurrent programs is complicated by the possibility of interferences happening between any two instructions of a task (pervasive interference), and these interferences not giving out any information about the behaviors of potentially interfering concurrent tasks (oblivious interference). Reasoning about a concurrent program would be easier if a programmer, modularly and statically (1) knows precisely the program points at which interferences may happen (sparse interference), and (2) has some insights into behaviors of potentially interfering tasks at these points (cognizant interference). In this work we present Panini, a core concurrent calculus which guarantees sparse interference, by controlling sharing among concurrent tasks, and cognizant interference, by controlling dynamic name bindings and accessibility of states of tasks. Panini promotes capsule-oriented programming whose concurrently running capsules own their states, communicate by asynchronous invocations of their procedures and dynamically transfer ownership. Panini limits sharing among two capsules to other capsules and futures, limits accessibility of a capsule states to only through its procedures and dispatches a procedure invocation on the static type of its receiver capsule. We formalize Panini, present its semantics and illustrate how its interference model, using behavioral contracts, enables Hoare-style modular reasoning about concurrent programs with interference.

ACM Reference

Bagherzadeh, M. and Rajan, H. 2015. Panini: A Concurrent Programming Model for Solving Pervasive and Oblivious Interference. Proceedings of the 14th International Conference on Modularity, MODULARITY, Fort Collins, USA (2015), 93–108.

BibTeX Reference

@inproceedings{BagherzadehRajan2015,
  author = {Mehdi Bagherzadeh and Hridesh Rajan},
  title = {Panini: A Concurrent Programming Model for Solving Pervasive and Oblivious Interference},
  booktitle = {Proceedings of the 14th International Conference on Modularity, MODULARITY, Fort Collins, USA},
  pages = {93--108},
  year = {2015},
  publisher = {{ACM}},
  editor = {Robert B. France and Sudipto Ghosh and Gary T. Leavens},
  doi = {10.1145/2724525.2724568},
  abstract = {
  Modular reasoning about concurrent programs is complicated by the possibility
  of interferences happening between any two instructions of a task (pervasive
  interference), and these interferences not giving out any information about
  the behaviors of potentially interfering concurrent tasks (oblivious
  interference). Reasoning about a concurrent program would be easier if a
  programmer, modularly and statically (1) knows precisely the program points at
  which interferences may happen (sparse interference), and (2) has some
  insights into behaviors of potentially interfering tasks at these points
  (cognizant interference). In this work we present Panini, a core concurrent
  calculus which guarantees sparse interference, by controlling sharing among
  concurrent tasks, and cognizant interference, by controlling dynamic name
  bindings and accessibility of states of tasks. Panini promotes
  capsule-oriented programming whose concurrently running capsules own their
  states, communicate by asynchronous invocations of their procedures and
  dynamically transfer ownership. Panini limits sharing among two capsules to
  other capsules and futures, limits accessibility of a capsule states to only
  through its procedures and dispatches a procedure invocation on the static
  type of its receiver capsule. We formalize Panini, present its semantics and
  illustrate how its interference model, using behavioral contracts, enables
  Hoare-style modular reasoning about concurrent programs with interference.},
}