Fair Cooperative Multithreading

Abstract. We propose a new operational model for shared variable concurrency, in the context of a concurrent, higher-order imperative language `a 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 ou...

• Type: Conference
• Year: 2007
• Where: CONCUR
• Authors: Gérard Boudol
• Keywords: CONCUR 2007, Realizability Interpretation, Realizability Technique, Variable Concurrency