In this paper all aspects of the coordination layer of Hume is formalised in Lamport’s TLA logic [1]. This layer use a
scheduling strategy called lock-step scheduling. It is followed by a formal definition of two other scheduling strategies:
• A staged scheduling which has efficiency benefits for certain program.
• A hierarchical scheduling which add structure to programs.
The main contribution of this paper is the full formalisation of this three scheduling strategies in TLA, and the proof
that staged and hierarchical scheduling are conservative extension of lock-step scheduling.
The last chapter illustrates the benefits hierarchical scheduling has when transforming programs, by showing an
example of a standard Hume transformation in Hierarchical Hume.
Familiarity with both Hume and TLA is assumed.