Notice

The website of Tom Schrijvers has moved to http://people.cs.kuleuven.be/~tom.schrijvers. Please adjust any links you maintain as this copy will be taken down shortly.


MRI: Modular Reasoning about Interference in Incremental Programming


C.d.S. Oliveira, Bruno and Schrijvers, Tom and Cook, William R..
In JOURNAL OF FUNCTIONAL PROGRAMMING, 22:6, pp. 797--852, 2012.

Abstract

Incremental Programming (IP) is a programming style in which new program components are defined as increments of other components. Examples of IP mechanisms include: Object-oriented programming (OOP) inheritance, aspect-oriented programming (AOP) advice and feature-oriented programming (FOP). A characteristic of IP mechanisms is that, while individual components can be independently defined, the composition of components makes those components become tightly coupled, sharing both control and data flows. This makes reasoning about IP mechanisms a notoriously hard problem: modular reasoning about a component becomes very difficult; and it is very hard to tell if two tightly coupled components interfere with each other's control and data flows. This paper presents modular reasoning about interference (MRI), a purely functional model of IP embedded in Haskell. MRI models inheritance with mixins and side-effects with monads. It comes with a range of powerful reasoning techniques: equational reasoning, parametricity and reasoning with algebraic laws about effectful operations. These techniques enable modular reasoning about interference in the presence of side-effects. MRI formally captures harmlessness, a hard-to-formalize notion in the interference literature, in two theorems. We prove these theorems with a non-trivial combination of all three reasoning techniques.

BibTeX

@article{jfp_mri,
  author = {C.d.S. Oliveira, Bruno and Schrijvers, Tom and Cook, William R.},
  title = {{MRI: Modular Reasoning about Interference in Incremental Programming}},
  journal = {JOURNAL OF FUNCTIONAL PROGRAMMING},
  volume = {22},
  number = {6},
  pages = {797--852},
  year = {2012},
  doi = {10.1017/S0956796812000354},
  url = {/Research/papers/jfp_mri.pdf},
  abstract = {Incremental Programming (IP) is a programming style in which
new program components are defined as increments of other components. 
Examples of IP mechanisms include: Object-oriented
programming (OOP) inheritance, aspect-oriented programming
(AOP) advice and feature-oriented programming (FOP).  A
characteristic of IP mechanisms is that, while individual components can be
independently defined, the composition of components makes those components
become tightly coupled, sharing both control and data flows.
This makes reasoning about IP mechanisms a notoriously hard problem:
modular reasoning about a component becomes very difficult; and 
it is very hard to tell if two tightly coupled components interfere 
with each other's control and data flows.

This paper presents modular reasoning about interference (MRI),
a purely functional model of IP
embedded in Haskell. MRI models inheritance with mixins and
side-effects with monads. It comes with a range of powerful reasoning techniques:
equational reasoning, parametricity and reasoning with algebraic laws about
effectful operations. These techniques enable modular reasoning about interference in the
presence of side-effects. 

MRI formally captures harmlessness, a hard-to-formalize notion
in the interference literature, in two theorems. We prove these theorems
with a non-trivial combination of all three reasoning techniques. 
  },
}