[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.
