[TYPES/announce] A paper on "Fair cooperative multithreading"

[Gerard Boudol]

A paper on "Fair cooperative multithreading, or: Typing termination in a 
higher-order concurrent imperative language" is available at the url

http://www-sop.inria.fr/mimosa/Gerard.Boudol/#fcm

This is an extended version, with proofs, of a paper with the same title 
published in the proceedings of CONCUR'07. The abstract is appended 
below. As always, comments are welcome.

Best wishes,

Gérard Boudol

Abstract:

We propose a new operational model for shared variable concurrency, in 
the context of a concurrent, higher-order imperative language à la ML.  
In our model the scheduling of threads is cooperative, and a 
non-terminating process suspends itself on each recursive call.  A 
property to ensure in such a model is fairness, that is, any thread 
should yield the scheduler after some finite computation.  To this end, 
we follow and adapt the classical method for proving termination in 
typed formalisms, namely the realizability technique.  There is a 
specific difficulty with higher-order state, which is that one cannot 
define a realizability interpretation simply by induction on types, 
because applying a function may have side-effects at types not smaller 
than the type of the function. Moreover, such higher-order side-effects 
may give rise to computations that diverge without resorting to explicit 
recursion. We overcome these difficulties by introducing a type and 
effect system for our language that enforces a stratification of the 
memory. The stratification prevents the circularities in the memory that 
may cause divergence, and allows us to define a realizability 
interpretation of the types and effects, which we then use to prove the 
intended termination property. Our realizability interpretation also 
copes with dynamic thread creation.