Section F) Restrictions and assumptions

This text cover the following topics:

F.1) Shared resources in -core
F.2) C-inlining and linking in -core
F.3) Timing semantics in -core and -cOOre

F.1) Shared resources in -core

Only one single task may execute in each (named) critical section. Sections may be hierarchically nested. This allows controlling side-effects, such as state updates, and message passing. The former typically used to protect shared variables/data from race conditions, while the second to control and sequence communication internally (messages) and to the environment (writing of ports).

F.2) C-inlining and linking in -core

In the -core language, C-code can both be arbitrarily embedded (inlined) as well as linked for creating an executable. The -core compiler does not attempt to analyse the logic of the embedded or linked C-code. This is a deliberate decision, C-code in general is beyond reasoning.

The programmer should be aware that parameters, e.g., sync(x)/async(x), actually amounts to inlining of C, code.

F.3) Timing semantics

In the following we denote a task instance as a task for brevity.
  • We define the permissible execution window for a task ti to be the range in time from it absolut baseline bl(ti) to the absolute time bl(ti) + its relative deadline dl(ti).
  • We assume a valid system to be schedulable, i.e., all tasks will execute within their permissible execution windows. We also assume that our run-time system successfully fulfils this requirement if not else stated.
  • We assume each task ti to be associated with a deadline dl(ti) being equal or smaller than the inter-arrival ia(ti) of the task ti. (Not necessary condition for schedulability but we exploit this in our run-time system implementations.)
  • For a postponed message/sub-task (async after X tj), sent from a task ti with dl(ti), tj is given the deadline dl(tj)=dl(ti)-X, i.e., a sub-task will be performed under the deadline of the sender if not explicitly set. This allows straightforward reasoning on the response time of a task, even it defers computations (which opens up for parallel execution).
  • For a message async tj sent by ti we inherit the execution window bl(tj)=bl(i), dl(ti)=dl(tj).
  • For a postponed message/sub-task (async after X before Y tj) a new permissible execution windows is created, with bl(tj)=X and dl(tj)=Y.
  • For a postponed message/sub-task (async after X tj) forming a cyclic chain, we offset the baseline bl(tj)=bl(ti)+X, and inherit the deadline dl(tj)=dl(ti), (ti is the head of the cyclic chain, not necessarily the sender). Currently -core analysis, code generation, and run-time systems do not implement this feature.

Words from the author:

Semantics for resources (critical section) are not to be considered final. In particular, wether a critical section may be recursive (reclaiming an already claimed resource) or not is yet to be decided on. On the one hand, given proper usage, it allows for increased flexibility, on the other, what would proper use be? E.g., given that we operate on a resource R used to protect a point (x,y), is it then proper to assign x, perform some operation on the point (x,y) (deferred to a function claiming R), and then assign y. Maybe not, if (x,y) is supposed to treated a point. And if not considered proper, could we reject such cases, and allow for other? We are not the first to dwell on this problem, but we seek a single well motivated semantics. (E.g., Pthreads, takes the rout of multiple semantics, and lets the mutex type decide. This ultimately adds to the confusion reasoning on pthread code, since you cannot deduce its semantics without looking at the complete system implementation, another case of flexibility before reasoning.)

Timing semantics are experimental, and needs to be formalised and proven sound/consistent. One can think of extensions allowing for emitting messages with baseline being the current time (i.e., create a time stamped interrupt), and the possibility to enforce rendez vous synchronisation.

Another potential extension, is to allow aborting messages that have been emitted but not yet started. To this end, the async will need to return a "hook" allowing abortion.

Time stamped messages, as well as message abortion will be studied by the students of Compiler Construction fall of 2014, and potentially added to the timing semantics merged into the distribution of our compilers.

Per Lindgren, founder of RTFM-lang, September 1st 2014

Last edited Sep 4, 2014 at 10:45 AM by RTFMPerLindgren, version 11