[PL-sem-jr] MONDAY 11/17: Christos on Future Contracts

[Aaron Turon]

Monday 11/17, Christos will talk about his research work on Future
Contracts.  The talk will take place in WVH166 from 1-3pm.

Upcoming talks:

  11/24 Ben: bounded model checking
  *12/2* Stephen: Milner's CCS
  12/8 Christos: Dpi, or the ambient calculus

Abstract:

Future Contracts
(with Riccardo Pucella and Matthias Felleisen)

Many recent research projects focus on language support for behavioral
software contracts, i.e., assertions that govern the boundaries
between software building blocks (procedures, classes, modules).
Unfortunately, as contracts become complex, they affect the
performance of the program.

In this paper, we introduce *future* contracts and concurrent contract
checking.  That is, software contracts annotated with *future* are
checked  concurrently with the main program, exploiting the now-common
multiple-core architecture. The paper presents both a model and a
prototype implementation of our language design. Our model comprises a
higher-order imperative language and we use it to prove the
correctness of our design. Our implementation is robust enough to
measure  the performance of reasonably large benchmarks, demonstrating
that the use of  *future* contracts can lead to significant
performance  improvements.