|
|
One considers the formal semantics of the cooperative part of
Loft. To simplify, one supposes that there is only one scheduler to
which all the created threads are linked. One first considers the
basic semantics, called Rewrite, then two variants of it, called
Replace and Optim. Replace puts the focus on memory use by
limiting the number of intermediate instructions that are created
during execution of an instant. The Optim variant puts the focus on
CPU usage, by avoiding busy-waiting on absent events.
The Rewrite variant is defined in the first 3 sections. The basics
of the semantics are introduced in Semantics Basics.
Then, one describes in Instructions in REWRITE the
semantics of expressions and of instructions. The semantics of threads
and schedulers is defined in
Threads and Schedulers in REWRITE.
The Replace variant is considered in REPLACE Semantics and the Optim variant in
OPTIM Semantics.
Finally, Conclusion concludes the
formal description of the language.
The semantics is expressed in the structural operational
semantics (SOS) format defined in [29]. First, one
defines the data structures corresponding to schedulers and
threads; then, an intuitive description of the semantics is given
to make the reading of the rest of the semantics easier; then, one
defines the various formats of the rewriting rules; finally, the
BNF syntax of the instructions is described.
5.1.1 Schedulers
A scheduler sched is a structure made of the following
components:
sched.linked is the list of threads linked
to the scheduler.
sched.current is the thread currently executed.
sched.events is the set of generated events.
sched.values is a table that associates to events
the list of values generated during the current instant.
sched.eoi is a boolean flag that indicates the end
of the current instant.
sched.move is a boolean flag that indicates the
need to postpone the end of the current instant.
sched.to_broadcast is the list of events and of
couples (event,value) that must be generated at the beginning of the
next instant.
sched.orders is the list of orders (stop, suspend,
resume, or link a thread) that must be executed at the beginning of
the next instant. Orders are build with the function order
which takes the kind of order as first parameter: STOP_ORDER,
SUSP_ORDER, RESUME_ORDER, or LINK_ORDER.
sched.to_finalize is the list of threads that
must be finalized.
One adopts the following notations:
sched<f = v> changes to v the
value of the field f of sched. For example, s<eoi = true> is equal to s, except that s.eoi
is set to true.
l += v adds the value v to the list l and sched<f += v> adds v to the field f (which must be a list or a set) of sched. In the same
way, l -= v removes the value v from l
and sched<f -= v>removes v from f in
sched.
- The list (or table) with no element in it is noted
Ø. The
nth element of a list l
is noted l(n), and the number of element of l is
noted length(l).
5.1.2 Threads
A thread th is a structure made of the following components:
th.run is the instruction run by the thread.
th.finalizer is the atomic instruction executed when
the thread is stopped.
th.suspended is a boolean which is true when the
thread is suspended.
th.state is the execution state of the thread:
- TERM: the thread is completely terminated.
- COOP: the thread cooperates.
- CONT: the thread needs to be continued during the
current instant. This is the initial state, and the one of a
thread waiting for an event which is not present, or trying to get
a non-available event value.
th.signal is an event used to signal the final
termination of the thread.
th.code is the return code set by some non-atomic
instructions. There are 3 possible codes:
- OK: the instruction has completed normally.
- ETIMEOUT: the limit has been reached (for
await
and join).
- ENEXT: not available value (for
get_value).
th.called denotes the thread created and executed when a
run non-atomic instruction is. Termination of this thread
is awaited by the calling thread.
An instance of a module is a new structure th. At creation,
th is such that:
th.suspended is false.
th.state is CONT.
th.signal is a new event.
th.run is a sequence made of the module body
followed by a generation of th.signal.
th.finalizer is the module finalizer.
th.code is OK.
th.called is NULL.
5.1.3 Overview of the Semantics
In this section, one gives an intuitive overview of the semantics.
Let's consider a scheduler sched and an environment env. The final goal of the semantics is to show without ambiguity
how sched and env evolve as time passes.
Actually, evolution is decomposed in a sequence of instants; the
first instant is:
which means that, starting from sched and env, one
gets sched1 and env1 at the end
of the instant.
Threads are not immediately started as soon as they are created in
order to avoid interferences with currently running threads. Actually,
all threads created during one instant are stored in sched.to_link, and are effectively started at the beginning of the
next instant. In the same way, events broadcast from the outside
world are stored in sched.to_broadcast and are incorporated
in the system at the beginning of the next instant. Stop, suspend, and
resume orders are processed in the same way. In case of stop orders,
finalizers of stopped threads are executed. Thus, evolution of the
scheduler as time passes is a sequence of the form:
|
|
| sched1', env1' | => | sched2, env2 |
|
| sched2', env2' | => | sched3, env3 |
|
| ... |
where schedi' incorporates in schedi all orders collected during instant i, and envi' is obtained from envi after
execution of finalizers of stopped threads.
Now, let's decompose instants: each instant consists in cyclically
running phases where all the threads are run in turn. Running
a thread t means to resume execution of its associated
instruction t.run. A thread which needs to be continued is
a non-suspended thread that has not already cooperated during the
instant. The instant is over when there is no such thread.
Threads which are started are placed in the linked list of
the scheduler. At the beginning of each instant, threads that are
terminated (TERM) and threads stopped during the previous instant
are removed from linked.
Note that the order in which the threads are executed always remains
the same during an instant. Note also that suspensions and resumptions
of threads never change the order in which the other threads are
executed.
The scheduler behavior consists in cyclically running the threads in
linked while there exist threads needing to be continued.
The number of phases depends on the events generated. For example,
consider a situation where linked = (t1,t2) and t1 awaits the event e
generated by t2. Then, after t2
execution, a new phase is needed to resume t1. Otherwise, t1 would not consider e as present despite the fact that it is generated; in such a
situation, one could not say that e is broadcast. Note that
a third phase would be necessary if, after generating e,
t2 is waiting for another event generated by t1. Actually, new phases are needed until one reaches a
situation where no new event is generated; then, the end of the
current instant can be safely decided.
The scheduler uses two boolean flags to manage instants:
- The flag
move is set each time a new event
is generated; it is reset by the scheduler at the beginning of
each phase. The scheduler does not decide the end of the current
instant when move is true, to give threads waiting for new
generated events the possibility to react to them.
- The flag
eoi is set by the scheduler when the end of
the current instant is decided; it is reset at the beginning of
each new instant. It is used to inform threads which are waiting for
events that these events are definitely absent. Then, the threads can
cooperate, and the next instant can safely take place.
Awaiting an event which is absent blocks a thread up to the end of the
current instant. This forbids immediate (that is, during the same
instant) reaction to the absence of an event; reaction, if any, is
thus postponed to next instant. This is important to avoid situations
where one could react to the absence of an event during one instant by
generating it during the same very instant, which would contradict the
fact that the event is absent. These kind of contradictions, known as
"causality problems" in synchronous languages [19],
do not exist here. In the same way, trying to get a not available
generated value blocks a thread up to the end of the current instant.
5.1.4 Rewriting Rules Formats
In this section, one gives the various formats of the rewriting rules
used in the semantics.
Instructions
The format of the rewritings of instructions is:
| | s | |
| inst, sched, env | → | inst', sched', env' |
In such a rewriting, the initial instruction is inst, the
scheduler sched, and the environment of data env. As a result, the rewriting produces a status s, a
new instruction inst', a new scheduler sched' and
a new environment env'.
There are 4 possible status:
- TERM: the instruction is terminated.
- COOP: the instruction cooperates.
- CONT: the instruction needs to be continued. It is the
status of an instruction waiting for an event which is not
present, or trying to get a non-available event value.
- RETURN: a return instruction has been reached.
Expressions
The notation for evaluating expressions is:
| exp | |= | sched, env | → | val, sched', env' |
The evaluation of exp, in the scheduler sched and
in the environment env, produces the value val,
and leads to the new scheduler sched' and to the new
environment env'.
Several expressions can be evaluated in one step. The notation is:
| (exp0,...,expn) | |= | sched, env | → | (val0,...,valn), sched', env' |
The evaluation of expi produces the value vali. The final scheduler is sched' and the
final environment is env'. The order in which the
expressions are evaluated is left unspecified.
Threads and Schedulers
The micro-step execution of a thread is noted:
| | | |
| th, sched, env | → | th', sched', env' |
At scheduler level, the execution of the thread number n is
noted:
| | | |
| sched, n, env | → | sched', env' |
A phase of the scheduler consists in executing in turn all the threads
linked in it. The format is:
Finally, an instant of the scheduler consists in cyclicly executing
phases up to a point where no thread needs to be continued. The format
is:
5.1.5 Syntax of Instructions
One gives the syntax of instructions considered in the semantics. The
syntax is very close to the real syntax of programs. However, we feel
free to make some simplifications when there is no deep impact over
the semantics (for example, in if instructions, the else branch is not optional). Some extensions are also included in
the syntax to ease the writing of the semantics rules (actually, these
extensions never appear in programs). The syntax of instructions
is:
inst =
inst ... inst
| atomic
| non-atomic
Atomic instructions execute completely in one single instant:
atomic =
{<c-code>}
| stop (exp)
| suspend (exp)
| resume (exp)
| generate (exp)
| generate (exp, exp)
Some special expressions are added to the ones of C:
exp =
special_exp
| <c-exp>
special_exp =
<module>_create (exp, ..., exp)
| return_code ()
| self ()
Execution of non-atomic instructions can last several instants:
non-atomic =
cooperate
| halt
| return
| await (exp)
| await (exp, exp)
| join (exp)
| join (exp,exp)
| get_value (exp, exp, exp)
| if (exp) then inst else inst end
| while (exp) do inst end
| repeat (exp) do inst end
| run <module> (exp, ..., exp)
| extensions
Some extensions are defined. They do not appear in real programs, but
are introduced as intermediary instructions:
extensions =
nothing
| repeat* (n, inst) do inst end
| while* (exp, inst) do inst end
| await* (event)
| await* (event, n)
| get_value* (event, n, v)
|
5.2 Instructions in REWRITE
|
One now considers the evaluation of expressions and the execution of
instructions in the basic semantics Rewrite.
5.2.1 Expressions
Expressions are evaluated in the standard way of C. However,
evaluation of some special expressions has an effect on the scheduler
(for example, the creation of threads) or are using it. Thus, the
general form of evaluation of expressions is:
| exp | |= | sched, env | → | value, sched', env' |
In this rewriting, value is the value obtained by evaluating
exp. The resulting scheduler is sched' and the
resulting environment is env'.
One now gives the semantics of special expressions.
Creation of Threads
New threads instances of a module m are created by calling
the function m_create.
| Rule 1: Create |
| (e1,...,en) | |= | sched, env | → | (v1,...,vn), sched', env' |
|
|
| m_create(e1,...,en) | |= | sched, env | → | t, sched'', env' |
|
| sched'' = sched'<orders += order (LINK_ORDER,t)> |
|
|
The thread t is a new thread created from the module m, with (v1,...,vn) as arguments. It
will be started only at the next instant.
Thread Code
A call to return_code returns the code of the current
thread.
| Rule 2: Return Code |
| return_code() | |= | sched, env | → | sched.current.code, sched, env |
|
|
Self
A call to self returns the executing thread which is
actually the current thread of the scheduler.
| Rule 3: Self |
| self() | |= | sched, env | → | sched.current, sched, env |
|
|
5.2.2 Sequence of Instructions
The semantics of sequences is contained in three rules. In the first
one, the execution of the first element of the sequence is not
terminated and thus only this element is changed in the resulting
instruction:
| Rule 4: Sequence - Not Term |
| | s | |
| i0, sched, env | → | i'0, sched', env' |
|
| s ≠ TERM |
|
| | s | |
| i0...in, sched, env | → | i'0...in, sched', env' |
|
|
|
The execution goes to the next component as soon as the previous one
terminates:
| Rule 5: Sequence - Term |
| | TERM | |
| i0, sched, env | → | i'0, sched', env' |
|
| | s | |
| i1...in, sched', env' | → | j, sched'', env'' |
|
|
| | s | |
| i0...in, sched, env | → | j, sched'', env'' |
|
|
|
Finally, one has also to consider for consistency reason the
degenerated case where the list is empty:
| Rule 6: Sequence - Empty |
| | TERM | |
| Ø, sched, env | → | Ø, sched, env |
|
|
5.2.3 Atomic Instructions
C Code
Standard C code enclosed in "{" and "}" is an atomic instruction,
executed in the standard way. This leads to rewritings of the form:
| | TERM | |
| {<c-code>}, sched, env | → | nothing, sched', env' |
Note that the scheduler can also be changed by execution of standard C
code because special expressions can appear in it.
Stop, Suspend, Resume
Execution of stop(t) adds the order to stop t to
the list of orders.
| Rule 7: Stop |
| e | |= | sched, env | → | t, sched', env' |
|
|
| | TERM | |
| stop(e), sched, env | → | nothing, sched'', env' |
|
| sched'' = sched'<orders += order (STOP_ORDER,t)> |
|
|
Execution of suspend(t) adds the order to suspend t to the list of orders.
| Rule 8: Suspend |
| e | |= | sched, env | → | t, sched', env' |
|
|
| | TERM | |
| suspend(e), sched, env | → | nothing, sched'', env' |
|
| sched'' = sched'<orders += order (SUSPEND_ORDER,t)> |
|
|
Execution of resume(t) adds the order to resume t
to the list of orders.
| Rule 9: Resume |
| e | |= | sched, env | → | t, sched', env' |
|
|
| | TERM | |
| resume(e), sched, env | → | nothing, sched'', env' |
|
| sched'' = sched'<orders += order (RESUME_ORDER,t)> |
|
|
Generate
A generate statement adds the generated event in the event
set of the scheduler, and immediately terminates; moreover, the
flag move is set to indicate that something new happened:
| Rule 10: Generate - Pure |
| e | |= | sched, env | → | v, sched', env' |
|
|
| | TERM | |
| generate(e), sched, env | → | nothing, sched'', env' |
|
| sched'' = sched'<move = true><events += v> |
|
|
Moreover, when a value is associated to the generation, it is added at
the end of the table of values associated to the event.
| Rule 11: Generate - Valued |
| (e1, e2) | |= | sched, env | → | (v1,v2), sched1, env1 |
|
| | TERM | |
| generate(v1), sched1, env1 | → | nothing, sched2, env2 |
|
|
| | TERM | |
| generate(e1, e2), sched, env | → | nothing, sched3, env2 |
|
| sched3 = sched2<val(v1) += v2> |
|
|
5.2.4 Non-Atomic Instructions
Cooperate, Halt, Nothing, Return
The cooperate statement finishes execution for the current
instant and returns COOP. Nothing remains to be done at the next
instant (thus, execution at the next instant will resume in sequence
from the cooperate instruction):
| Rule 12: Cooperate |
| | COOP | |
| cooperate, sched, env | → | nothing, sched, env |
|
|
The halt instruction never terminates:
| Rule 13: Halt |
| | COOP | |
| halt, sched, env | → | halt, sched, env |
|
|
The following rule is introduced for completeness; actually, the
nothing instruction does not appear in real programs.
| Rule 14: Nothing |
| | TERM | |
| nothing, sched, env | → | nothing, sched, env |
|
|
The return instruction forces the termination of the
executing thread by returning the status RETURN. It also generates
the event which signals the thread termination:
| Rule 15: Return |
| | TERM | |
| generate (sched.current.signal), sched, env | → | nothing, sched', env' |
|
|
| | RETURN | |
| return, sched, env | → | nothing, sched', env' |
|
|
|
Await
An instruction await first determines which event is awaited
and then behaves as await*:
| Rule 16: Await |
| e | |= | sched, env | → | v, sched', env' |
|
| | s | |
| await* (v), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| await (e), sched, env | → | i, sched'', env'' |
|
|
|
The waiting terminates when the awaited event is present:
| Rule 17: Await - Present |
| v ∈ sched.events |
|
| | TERM | |
| await* (v), sched, env | → | nothing, sched, env |
|
|
|
Execution needs to be continued during the same instant when the
awaited event is unknown (neither present nor absent):
| Rule 18: Await - Unknown |
| v not in sched.events |
| sched.eoi = false |
|
| | CONT | |
| await* (v), sched, env | → | await* (v), sched, env |
|
|
|
The await instruction cooperates when the awaited event is
absent. The absence is detected because the event is not generated
while the end of the current instant has been decided:
| Rule 19: Await - Absent |
| v not in sched.events |
| sched.eoi = true |
|
| | COOP | |
| await* (v), sched, env | → | await* (v), sched, env |
|
|
|
Limited Await
With a limited await, the waiting is limited to a fixed
number of instants:
| Rule 20: Limited Await |
| (e1,e2) | |= | sched, env | → | (v,n), sched', env' |
|
| | s | |
| await* (v,n), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| await (e1,e2), sched, env | → | i, sched'', env'' |
|
|
|
Rules for the limited await are very similar to the ones of the
standard await, except that tests for the delay are
introduced.
The instruction immediately terminates when the delay is over, and in
this case, the return code of the executing thread is set to ETIMEOUT.
| Rule 21: Limited Await - Over |
| n ≤ 0 |
|
| | TERM | |
| await* (v,n), sched, env | → | nothing, sched', env |
|
| sched' = sched<current.code = ETIMEOUT> |
|
|
The instruction also immediately terminates when the awaited event is
present; in this case, the return code of the executing thread is
set OK.
| Rule 22: Limited Await - Present |
| n > 0 |
| v ∈ sched.events |
|
| | TERM | |
| await* (v,n), sched, env | → | nothing, sched', env |
|
| sched' = sched<current.code = OK> |
|
|
The executing thread needs to be continued during the current instant while
the awaited is unknown.
| Rule 23: Limited Await - Unknown |
| n > 0 |
| v not in sched.events |
| sched.eoi = false |
|
| | CONT | |
| await* (v,n), sched, env | → | await* (v,n), sched, env |
|
|
|
The executing thread cooperates when the awaited event is absent. This
can only happen at the end of the instant. In this case, the waiting
delay is decremented.
| Rule 24: Limited Await - Absent |
| n > 0 |
| v not in sched.events |
| sched.eoi = true |
|
| | COOP | |
| await* (v,n), sched, env | → | await* (v,n-1), sched, env |
|
|
|
An important point must be noticed: the previous rules describe a
busy-waiting mechanism: actually, the await* instruction
should activated at each micro-step of each instant, until the awaited
event is present (except of course during instants where the executing
thread is suspended).
If
The if instruction chooses a branch accordingly to the value
of a boolean expression, and it executes it up to completion (which
may take several instants; note that the expression is evaluated
only once):
| Rule 25: If - True |
| e | |= | sched, env | → | true, sched', env' |
|
| | s | |
| i, sched', env' | → | i', sched'', env'' |
|
|
| | s | |
| if (e) then i else j end, sched, env | → | i', sched'', env'' |
|
|
|
| Rule 26: If - False |
| e | |= | sched, env | → | false, sched', env' |
|
| | s | |
| j, sched', env' | → | j', sched'', env'' |
|
|
| | s | |
| if (e) then i else j end, sched, env | → | j', sched'', env'' |
|
|
|
While
A while loop first evaluates the associated boolean
expression and terminates if the returned value is false:
| Rule 27: While - False |
| e | |= | sched, env | → | false, sched', env' |
|
|
| | TERM | |
| while (e) do i end, sched, env | → | nothing, sched', env' |
|
|
|
Otherwise, the loop behaves as the auxiliary while* loop
defined below:
| Rule 28: While - True |
| e | |= | sched, env | → | true, sched', env' |
|
| j = while* (e, i) do i end |
| | s | |
| j, sched', env' | → | j', sched'', env'' |
|
|
| | s | |
| while (e) do i end, sched, env | → | j', sched'', env'' |
|
|
|
The auxiliary while* instruction runs the loop body up to
termination, without re-evaluating the boolean condition; then, it
rewrites as a standard while loop which evaluates the
condition to determine if the body has to be run one more time.
| Rule 29: While - Not Term |
| | s | |
| i, sched, env | → | i', sched', env' |
|
| s ≠ TERM |
|
| | s | |
| while* (e, init) do i end, sched, env | → | j, sched', env' |
|
| j = while* (e, init) do i' end |
|
|
| Rule 30: While - Term |
| | TERM | |
| i, sched, env | → | i', sched', env' |
|
| | s | |
| while (e) do init end, sched', env' | → | j, sched'', env'' |
|
|
| | s | |
| while* (e, init) do i end, sched, env | → | j, sched'', env'' |
|
|
|
Repeat
A repeat loop executes its body a limited number of
times. This number is the value of an expression which is first
evaluated:
| Rule 31: Repeat |
| e | |= | sched, env | → | n, sched', env' |
|
| j = repeat* (n, i) do i end |
| | s | |
| j, sched', env' | → | j', sched'', env'' |
|
|
| | s | |
| repeat (e) do i end, sched, env | → | j', sched'', env'' |
|
|
|
The loop terminates when the number of cycles to be performed is negative:
| Rule 32: Repeat - Negative |
| n ≤ 0 |
|
| | TERM | |
| repeat* (n, init) do i end, sched, env | → | nothing, sched, env |
|
|
|
Otherwise, the loop behaves as its body when it does not terminates:
| Rule 33: Repeat - Not Term |
| 0 < n |
| | s | |
| i, sched, env | → | i', sched', env' |
|
| s ≠ TERM |
|
| | s | |
| repeat* (n, init) do i end, sched, env | → | j, sched', env' |
|
| j = repeat* (n, init) do i' end |
|
|
When the body terminates, the number of cycles to be performed is
decremented and the loop is immediately restarted.
| Rule 34: Repeat - Term |
| 0 < n |
| | TERM | |
| i, sched, env | → | i', sched', env' |
|
| j = repeat* (n-1, init) do init end |
| | s | |
| j, sched', env' | → | j', sched'', env'' |
|
|
| | s | |
| repeat* (n, init) do i end, sched, env | → | j', sched'', env'' |
|
|
|
Get Value
The get_value instruction returns the with index
n (it it exists) associated to a given event. First, three
expressions are evaluated: the event, the index n, and the
place where the result should be placed.
| Rule 35: Get Value |
| (e1,e2,e3) | |= | sched, env | → | (v,n,r), sched', env' |
|
| | s | |
| get_value* (v,n,r), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| get_value (e1,e2,e3), sched, env | → | i, sched'', env'' |
|
|
|
The instruction immediately terminates if the value is available. In
this case, the value is assigned to the result variable and the return
code of the executing thread is set to OK.
| Rule 36: Get Value - Available |
| length(sched.values(v)) > n |
|
| | TERM | |
| get_value* (v,n,r), sched, env | → | nothing, sched', env' |
|
| sched' = sched<current.code = OK> |
| env' = env<r = (sched.values(v))(n)> |
|
|
The instruction has to be continued if the value is not available
while the current instant is not terminated:
| Rule 37: Get Value - Unknown |
| length(sched.values(v)) ≤ n |
| env.eoi = false |
|
| | CONT | |
| get_value* (v,n,r), sched, env | → | get_value* (v,n,r), sched, env |
|
|
|
The instruction cooperates if the value is still not available at the
end of the current instant. In this case, the return code is set to
ENEXT which will indicate at the next instant that the value has not
been got.
| Rule 38: Get Value - Not Available |
| length(sched.values(v)) ≤ n |
| env.eoi = true |
|
| | COOP | |
| get_value* (v,n,r), sched, env | → | nothing, sched', env |
|
| sched' = sched<current.code = ENEXT> |
|
|
Join
Nothing is done if the thread to be joined is already terminated:
| Rule 39: Join - Terminated |
| e | |= | sched, env | → | t, sched', env' |
|
| t.state = TERM |
|
| | TERM | |
| join (e), sched, env | → | nothing, sched', env' |
|
|
|
Otherwise, the instruction waits for the event which is generated when
the thread terminates (see Threads):
| Rule 40: Join - Not Terminated |
| e | |= | sched, env | → | t, sched', env' |
|
| t.state ≠ TERM |
| | s | |
| await* (t.signal), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| join (e), sched, env | → | i, sched'', env'' |
|
|
|
Limited Join
Limited join is similar to join, except that the
delay is also tested for termination. The instruction immediately
terminates if the thread to be joined is already terminated. In this
case, the return code of the executing thread is set to OK.
| Rule 41: Limited Join |
| (e1,e2) | |= | sched, env | → | (t,n), sched', env' |
|
| t.state = TERM |
|
| | TERM | |
| join (e1, e1), sched, env | → | nothing, sched'', env' |
|
| sched'' = sched'<current.code = OK> |
|
|
If the thread to be joined is not already terminated, then the termination
event is awaited.
| Rule 42: Limited Join - Waiting |
| (e1,e2) | |= | sched, env | → | (t,n), sched', env' |
|
| th.state ≠ TERM |
| | s | |
| await* (t.signal, n), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| join (e1, e2), sched, env | → | i, sched'', env'' |
|
|
|
Run
To run a module means to create a new instance of the module and to
join it. Moreover, the instance is stored in the component called of the calling thread in order to be stopped when the
calling thread is.
| Rule 43: Run |
| m_create (e1,..., en) | |= | sched, env | → | t, sched', env' |
|
| sched1 = sched'<current.called = t> |
| | s | |
| join (t), sched1,env' | → | i, sched2, env2 |
|
|
| | s | |
| run m (e1,..., en), sched, env | → | i, sched2, env2 |
|
|
|
|
5.3 Threads and Schedulers in REWRITE
|
The semantics of threads and schedulers in Rewrite is now
considered. One defines some auxiliary functions using a very
simple self-explanatory syntax.
5.3.1 Threads
First, one defines the firing of a thread. A thread is fireable if it is not suspended and if its state is CONT:
fireable (thread)
return thread.suspended = false and thread.state = CONT
To fire a fireable thread means to rewrite its body and to force the
state to TERM if the rewriting produces RETURN.
| Rule 44: Fireable Thread |
| fireable (t) = true |
| | s | |
| t.run, sched, env | → | i, sched', env' |
|
|
| | | |
| t, sched, env | → | t', sched', env' |
|
| t' = t<run = i>
<state = (if s = RETURN then TERM else s)> |
|
|
To fire a thread which is not fireable has no effect.
| Rule 45: Not Fireable Thread |
| fireable (t) = false |
|
| | | |
| t, sched, env | → | t, sched, env |
|
|
|
5.3.2 Schedulers
During a phase, the scheduler performs a sequence of steps in which it
fires all the threads linked to it. The nth step consists in
firing the nth thread, considering it as the current thread of
the scheduler:
| Rule 46: Nth Thread |
| length(sched.linked) > n |
| t = sched.linked(n) |
| | | |
| t, sched<current = t>, env | → | t', sched', env' |
|
|
| | | |
| sched, n, env | → | sched'<linked(n) = t'>, env' |
|
|
|
One now switches to the rules describing phases. The first rule
corresponds to an empty scheduler. In this case, nothing is done
during the phase:
| Rule 47: Scheduler - Empty |
|
|
|
Otherwise, when the scheduler is not empty, all the threads are fired
in turn:
| Rule 48: Scheduler - Not Empty |
| length(sched.linked) = n+1 |
| | | |
| sched, 0, env | → | sched1, env1 |
|
| | | |
| sched1, 1, env1 | → | sched2, env2 |
|
| ... |
| | | |
| schedn, n, envn | → | sched', env' |
|
|
|
|
|
|
Note that threads are considered in a fixed order, which is the order
of appearance in linked.
5.3.3 Instants
Instants are macro-steps of schedulers. Basically, an instant is a
sequence of phases leading to a stable situation, where no thread
remains to be continued. One first defines the function stable that determines if a scheduler is in a stable situation or
not.
stable (sched)
forall thread in sched.linked
if (fireable (thread)) return false
return true
The first rule corresponds to a phase leading to a stable
situation. In this case, execution for the current instant is over.
| Rule 49: Instant - Finished |
|
|
|
If the phase leads to an unstable situation, then the scheduler
cyclically re-schedule all the threads. If no event is generated
during a phase (move is still false at the end of the
phase), then the scheduler decides that the current instant can be
finished by setting the flag eoi to true.
| Rule 50: Instant - Not Finished |
|
|
| stable (sched') = false |
| make_decision(sched'), env' | => | sched'', env'' |
|
|
| sched, env | => | sched'', env'' |
|
|
|
where the function make_decision is:
make_decision (sched)
if (sched.move = true) return sched<move = false>
else return sched<eoi = true>
5.3.4 Inter Instants Processing
One finally considers the chaining of instants and more specifically
the actions performed between two successive instants. Actually, these
actions are regrouped at beginnings of instants and are specified by
the function start_instant.
The call start_instant(sched,env) resets the two flags
eoi and move of the scheduler and incorporates in
sched the events and orders that have been produced (by the
program or by the external world) during the previous instant; then it
removes the terminated threads and resets those that are not suspended;
finally, it finalize the stopped threads:
start_instant (sched,env)
sched.eoi = false
sched.move = false
transfer_events (sched)
process_orders (sched,env)
reset_threads (sched)
finalize_stopped_threads (sched)
Transfer Events
The transfer_events functions sets the events and the table
of values associated to them, according to the broadcast orders.
transfer_events (sched)
sched.events = get_events (to_broadcast)
sched.val = get_values (to_broadcast)
sched.to_broadcast = Ø
The call get_events (x) returns the list of events extracted
from x; get_values (x) returns the table build
from the couples (event,value) belonging to x.
Note that previous elements of events are lost; this is
coherent as events are always resets at the beginning of each new
instant.
Processing Orders
The various orders (others than the broadcast ones) are processed
in turn by the function process_orders.
process_orders (sched,env)
forall order in previous
if (order.kind = SUSPEND_ORDER)
order.thread.suspended = true
else if (order.kind = RESUME_ORDER)
order.thread.suspended = false
else if (order.kind = STOP_ORDER)
sched.to_finalize += thread
thread.state = TERM
else if (order.kind = LINK_ORDER)
sched.linked += order.thread
sched.orders = Ø
Stopped threads are places into the to_finalize list in
order to be processed later. Thus, orders issued from finalizer
execution will be performed at the next instant, and not during the
current one. As a consequence, no instantaneous can occur from a
finalizer sending orders to the scheduler running it.
Reset Threads
The function reset_threads eliminates from linked
the threads that are terminated or unlinked and sets to CONT the
status of the remaining threads that are not suspended.
reset_threads (sched)
forall thread in sched.linked
if (thread->state = TERM)
sched.linked -= thread
else if (thread->suspended = false and thread->state = COOP)
thread.state = CONT
Finalization
To finalize a thread means to set its state to TERM, to add the
signaling event in the list of events, to call the finalizer of the
thread, and finally to recursively finalize the called thread, if
there is one.
finalize (sched,env,thread)
if (thread.state = TERM) return
thread.state = TERM
sched.events += thread.signal
sched = sched'
env = env'
if (thread.called != NULL) finalize (sched,env,thread.called)
where sched',env' results from the execution of thread.finalizer in sched,env:
| | TERM | |
| thread.finalizer, sched, env | → | nothing, sched', env' |
All threads which must be finalized are processed by the scheduler in
turn:
finalize_stopped_threads (sched)
forall thread in sched.to_finalize
finalize (thread)
sched.to_finalize = Ø
This ends with the inter-instant actions that are performed by
the scheduler at each beginning of instant.
Chaining Instants
Finally, the execution accross instants, starting from an environment
env, of a scheduler sched is a chain of rewritings
of the form:
|
|
| start_instant(sched1,env1),
| => | sched2, env2 |
|
| start_instant(sched2,env2),
| => | sched3, env3 |
|
| ... |
This concludes the description of the semantics Rewrite.
One now considers the Replace semantics, which is a variant of the basic
semantics Rewrite, designed to limit the creation of new instructions
during the rewriting process. Actually, no new instruction is created
by Replace during rewritings, and to rewrite an instruction basically
means to change its state.
5.4.1 Sequence
The first instruction to be considered is the sequence which receives
a state indicating which element is currently executed. One
introduces explicitely the sequence operator seq in order to
assign a state to it. The state is an integer which can be added as an
index to the sequence operator. The execution begins with the first
component (with index 0):
| Rule 51: Sequence - Init |
| | s | |
| seq0 (i0, ..., in), sched, env | → | i, sched', env' |
|
|
| | s | |
| seq (i0, ..., in), sched, env | → | i, sched', env' |
|
|
|
Execution stays in the same component while it is not terminated:
| Rule 52: Sequence - Stay |
| | s | |
| ik, sched, env | → | i'k, sched', env' |
|
| s ≠ TERM |
|
| | s | |
| seqk (i0, ...,
ik, ...,
in), sched, env | → | j, sched', env' |
|
| j = seqk (i0, ...,
i'k, ...,
in) |
|
|
Execution goes to the next component as soon as the current one terminates:
| Rule 53: Sequence - Next |
| | TERM | |
| ik, sched, env | → | i'k, sched', env' |
|
| | s | |
| seqk+1 (i0, ...,
in), sched', env' | → | i'', sched'', env'' |
|
|
| | s | |
| seqk (i0, ..., in), sched, env | → | i'', sched'', env'' |
|
|
|
Finally, execution terminates when the last component does:
| Rule 54: Sequence - Term |
| | TERM | |
| seqn+1 (i0, ..., in), sched, env | → | seqn+1 (i0, ..., in), sched, env |
|
|
5.4.2 Atomic Instructions
Atomic instructions have no state but always rewrite in themselves,
producing the status TERM. Actually, the execution which passes
through an atomic instruction is under control of the instruction
which encloses it (typically, a sequence). One just gives the rule for
C code:
| | TERM | |
| {<c-code>}, sched, env | → | {<c-code>}, sched', env' |
Note that now the atomic instruction does not anymore rewrite in
nothing, but in the same instruction.
5.4.3 Non-Atomic Instructions
Non-atomic instructions have states. We only give the semantics of
some of them to show the introduction of states and the way they are
managed. The semantics of others instructions should be
straightforward.
Cooperate
The cooperate has a state which indicates if the control
has or not passed through the instruction. Actually, a simple tag is
needed. The cooperate statement returns COOP and sets
its state to return TERM at the next instant. One now has two
rules for cooperate:
| Rule 55: Cooperate |
| | COOP | |
| cooperate, sched, env | → | cooperatetrue, sched, env |
|
|
| Rule 56: Cooperate - Term |
| | TERM | |
| cooperatetrue, sched, env | → | cooperatetrue, sched, env |
|
|
Await
An await instruction has a state which stores the awaited event.
First, the awaited event is stored in the state:
| Rule 57: Await (State) |
| e | |= | sched, env | → | v, sched', env' |
|
| | s | |
| awaitv (e), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| await (e), sched, env | → | i, sched'', env'' |
|
|
|
The waiting terminates when the awaited event is present:
| Rule 58: Await - Present (State) |
| v ∈ sched.events |
|
| | TERM | |
| awaitv (e), sched, env | → | awaitv (e), sched, env |
|
|
|
Execution must be continued when the awaited event is unknown (neither
present nor absent):
| Rule 59: Await - Unknown (State) |
| v not in sched.events |
| sched.eoi = false |
|
| | CONT | |
| awaitv (e), sched, env | → | awaitv (e), sched, env |
|
|
|
Finally, the instruction cooperates when the awaited event is absent:
| Rule 60: Await - Absent (State) |
| v not in sched.events |
| sched.eoi = true |
|
| | COOP | |
| awaitv (e), sched, env | → | awaitv (e), sched, env |
|
|
|
Note that actually the difference with the corresponding rules of
Rewrite consists in the replacement by a state of the await*
extension of the syntax.
If
The if instruction chooses a branch, according to the value
of a boolean expression, and executes it up to completion. A boolean
state is added to store which branch is chosen:
| Rule 61: If |
| e | |= | sched, env | → | v, sched', env' |
|
| | s | |
| ifv(e) then i else j end, sched', env' | → | k, sched'', env'' |
|
|
| | s | |
| if (e) then i else j end, sched, env | → | k, sched'', env'' |
|
|
|
| Rule 62: If - True |
| | s | |
| i, sched, env | → | i', sched', env' |
|
|
| | s | |
| iftrue (e) then i else j end, sched, env | → | k, sched', env' |
|
| k = iftrue (e) then i' else j end |
|
|
| Rule 63: If - False |
| | s | |
| j, sched, env | → | j', sched', env' |
|
|
| | s | |
| iffalse (e) then i else j end, sched, env | → | k, sched', env' |
|
| k = iffalse (e) then i else j' end |
|
|
While
One major difference of Replace with Rewrite concerns the loops. In
Replace, loops bodies are not duplicated as in Rewrite (using the
extended instructions repeat* and while*), but are
reset at the end of each cycle, in order to be ready for the next
cycle. One only considers here while loops.
A while loop first evaluates the associated boolean
expression A state is introduced to store the fact that the expression
is evaluated or not. The state is actually a simple tag. The loop
terminates if the value of the expression is false:
| Rule 64: While - False |
| e | |= | sched, env | → | false, sched', env' |
|
|
| | TERM | |
| while (e) do i end, sched, env | → | while (e) do i end, sched', env' |
|
|
|
Otherwise, the loop sets its state:
| Rule 65: While - True |
| e | |= | sched, env | → | true, sched', env' |
|
| | s | |
| whiletrue (e) do i end, sched', env' | → | j, sched'', env'' |
|
|
| | s | |
| while (e) do i end, sched, env | → | j, sched'', env'' |
|
|
|
The body is run up to termination, without re-evaluating the boolean
condition.
| Rule 66: While - Not Term |
| | s | |
| i, sched, env | → | i', sched', env' |
|
| s ≠ TERM |
|
| | s | |
| whiletrue (e) do i end, sched, env | → | whiletrue (e) do i' end, sched', env' |
|
|
|
When the body terminates, it is reset using the reset
function defined in Reset Function, in order to
be re-executed from the beginning:
| Rule 67: While - Reset |
| | TERM | |
| i, sched, env | → | i', sched', env' |
|
| | s | |
| while (e) do reset(i) end, sched', env' | → | j, sched'', env'' |
|
|
| | s | |
| whiletrue (e) do i end, sched, env | → | j, sched'', env'' |
|
|
|
Join
The thread to be joined is first determined and stored in the
instruction state:
| Rule 68: Join |
| e | |= | sched, env | → | t, sched', env' |
|
| | s | |
| joint (e), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| join (e), sched, env | → | i, sched'', env'' |
|
|
|
Nothing is done if the thread is already terminated:
| Rule 69: Join - Terminated |
| t.status = TERM |
|
| | TERM | |
| joint (e), sched, env | → | joint (e), sched, env |
|
|
|
Otherwise, the instruction waits for the termination signal:
| Rule 70: Join - Waiting |
| t.status ≠ TERM |
| | s | |
| awaitt.signal (t.signal), sched, env | → | i, sched', env' |
|
|
| | s | |
| joint (e), sched, env | → | joint (e), sched', env' |
|
|
|
5.4.4 Reset Function
The reset function is used by loops to reset their body at
the beginning of each cycle. To reset a term actually means to erase all indices appearing in it. The recursive definition of
reset is straightforward and is left to the reader.
For example, consider:
repeat3 (5) do
seq0 (
awaite (event),
cooperatetrue
)
end
The result of reseting the previous instruction is:
repeat (5) do
seq(
await (event),
cooperate
)
end
A strong property holds concerning the reset function: the
basis of an instruction, which is the instruction without any
indices in it, never changes during the rewriting process. That is,
one has:
| | s | |
| i, sched, env | → | i', sched', env' |
implies
reset(i) = reset(i').
In Replace, the rewriting is thus just a change of instruction
states. This is the reason why it can be implemented more efficiently
than Rewrite, without creation of new instructions during execution
(except of course when new threads are created).
One now considers a variant of the previous semantics Replace,
called Optim, in which threads are not busy-waiting for events. This
variant basically uses queues associated to events in which waiting
threads are stored. A special queue to store threads that are
submitted to deadlines (because they execute limited forms of await and join) is also defined. There are few changes
with the previous semantics and only the major ones are given in the
sequel.
First, one adds the new status WAIT to the possible ones returned
by the rewriting of instructions. This status corresponds to a
registration in a waiting queue. Second, one adds three new fields to
schedulers:
- A table, named
waiting (initially empty),
which associates to an event the list of threads waiting for it.
- An integer
instant which holds the current instant
number (initially 0).
- A list of threads, named
timer (initially empty),
whose elements are the threads waiting for a deadline.
Finally, a new field deadline is added to threads to
store the maximal instant to be considered by limited instructions.
5.5.1 Atomic Instructions
Amongst the atomic instructions, only the generate
instruction has to be changed. Indeed, in addition to what was
previously done, a generate statement awakes all the threads
waiting for the generated event:
| Rule 71: Generate - Pure |
| e | |= | sched, env | → | v, sched', env' |
|
|
| | TERM | |
| generate(e), sched, env | → | nothing, sched'', env' |
|
| sched'' = awake_all (sched',v)<move = true><events += v> |
|
|
The awake_all function awakes all the threads waiting for
the generated event:
awake_all (sched, event)
forall thread in sched.waiting (event)
awake (sched,thread,event)
return sched
To awake a thread means to change its state to CONT and to
unregister it from the queues where it is registered. Of course, this
is for threads that are effectively waiting for the event and that are
not suspended.
awakeable (thread)
return thread.suspended = false and thread.state = WAIT
The awake function is defined by:
awake (sched,thread,event)
if (awakeable (thread))
thread.state = CONT,
sched.waiting(event) -= thread
sched.timer -= thread
5.5.2 Non-Atomic Instructions
One only considers the changes concerning the await
statement (changes for other instructions are straightforward).
Await
An await instruction first determines the awaited event and
stores it in its state:
| Rule 72: Await |
| e | |= | sched, env | → | v, sched', env' |
|
| | s | |
| awaitv(e), sched', env' | → | i, sched'', env'' |
|
|
| | s | |
| await (e), sched, env | → | i, sched'', env'' |
|
|
|
The waiting terminates when the awaited event is present:
| Rule 73: Await - Present |
| v ∈ sched.events |
|
| | TERM | |
| awaitv(e), sched, env | → | awaitv(e), sched, env |
|
|
|
The executing thread is put in the state WAIT and registered in the
waiting list when the awaited event is not present:
| Rule 74: Await - Unknown |
| v not in sched.events |
|
| | WAIT | |
| awaitv(e), sched, env | → | awaitv(e), sched', env |
|
| sched' = sched<waiting(v) += sched.current> |
|
|
Limited Await
With a limited await, the waiting is limited to a fixed
number of instants:
| Rule 75: Limited Await |
| (e1,e2) | |= | sched, env | → | (v,n), sched', env' |
|
| sched1 = sched'<current.deadline = n + sched.instant> |
| | s | |
| awaitv(e1,e2),
sched1, env' | → | i, sched2, env2 |
|
|
| | s | |
| await (e1,e2), sched, env | → | i, sched2, env2 |
|
|
|
| Rule 76: Limited Await - Over |
| sched.current.deadline > sched.instant |
|
| | TERM | |
| awaitv(e1,e2), sched, env | → | awaitv(e1,e2), sched', env |
|
| sched' = sched<current.code = ETIMEOUT> |
|
|
| Rule 77: Limited Await - Present |
| sched.current.deadline ≤ sched.instant |
| v ∈ sched.events |
|
| | TERM | |
| awaitv(e1,e2), sched, env | → | awaitv(e1,e2), sched', env |
|
| sched' = sched<current.code = OK> |
|
|
When the waiting is effective, the current thread is registered in the
timer and in the waiting list associated to the awaited event:
| Rule 78: Limited Await - Unknown |
| t = sched.current |
| t.deadline ≤ sched.instant |
| v not in sched.events |
|
| | WAIT | |
| awaitv(e1,e2), sched, env | → | awaitv(e1,e2), sched', env |
|
| sched' = sched<waiting(v) += t><timer += t> |
|
|
5.5.3 Schedulers
The change in the scheduler concerns the processing of the timer which is
introduced in start_instant:
start_instant (sched,env)
sched.eoi = false
sched.move = false
timer_processing (sched)
transfer_events (sched)
process_orders (sched,env)
reset_threads (sched)
finalize_stopped_threads (sched)
where the function timer_processing is defined by:
timer_processing (sched)
sched.instant = sched.instant + 1
forall thread in sched.timer
if (awakeable (thread) and thread.deadline ≤ sched.instant)
awake (thread),
A point must be noted: to perform supplementary calls to the awake function is not dangerous, in the sense that it cannot change
the meaning of a program. Indeed, to awake a thread which has not to
be awaken will leads to reintroduce it into the game, and does not
change the actions that the thread has to perform. This basically
means that spurious awake actions are not a problem. The consequence
is that one can choose to never unregister threads from the timer,
without risk of perturbating the execution later. This actually can be
useful for optimizing implementations.
One has precisely defined the semantics of the cooperative part of
Loft using rewriting rules.
In a first step, one has described the semantics Rewrite with a set
of about 50 rules covering all the aspects of the cooperative part of
the language. The rules are simple to be understood one by one, and
one can be rather confident that they capture the essence of the
language. Actually, a way to make this confidence stronger is to
implement the semantics as is, and to execute tests covering the
largest possible set of various aspects of the language. This is of
course possible because the semantics is basically deterministic,
which allows one to implement it in a straightforward way.
A direct implementation of the semantics is however unsatisfactory
when considered in terms of efficiency for at least the following
reasons:
- A huge number of instructions appear as
intermediary results in the rules. From an implementation point of
view, they are wasting memory and should not be created at all.
- The threads are busy-waiting events, which waste CPU cycles.
Note that a thread which is waiting for an event tests for it at each
micro-step of each instant, up to the possible generation of it.
- Sequencing of instructions has to be explicitely executed, and
is not just implicit as for example in standard C.
- All the threads linked to a scheduler are considered in turn
during each phase. Thus, to determine which is the next thread to
execute is not constant in time, but linear in the number of threads
linked to the scheduler.
Actually, the main interest of Rewrite is to serve as a reference for
teaching and implementation purposes. Two improved semantics are defined
which model more efficient implementations.
The variant Replace of Rewrite is defined to deal with the first
previous point. In it, the construction of new instructions is
replaced by the introduction of states in instructions. Instead of
creating a new instruction from an old one, one just changes the state.
Replace is transformed to avoid busy-waiting (previous point 2),
using queues in which threads that are waiting for events are
stored. This leads to the variant Optim which is closer to an
efficient implementation of Loft than the previous semantics.
The two last points are not covered at the semantics level but will be
considered later in section Implementations, when
implementation of Loft is discussed.
To end with semantics concerns, one should notice that the
non-cooperative part of Loft is not considered by any of the
previous semantics. To cover the whole language, a way that should be
explored is the chemical abstract machine paradigm [10] to deal with nondeterministic aspects arising in this case.
|