Coordinating phased activities while maintaining progress

Abstract. In order to develop reliable applications for parallel ma-chines, programming languages and systems need to provide for flexi-ble parallel programming coordination techniques. Barriers, clocks and phasers constitute promising synchronisation mechanisms, but they ex-hibit intricate semantics and allow writing programs that can easily deadlock. We present an operational semantics and a type system for a fork/join programming model equipped with a flexible variant of phasers. Our proposal allows for a precise control over the maximum number of synchronisation steps each task can be ahead of others. A type system ensures that programs do not deadlock, even when they use multiple phasers.