Draft: Adding branch with critical sections. Changes to beahviour/schedule.v, new...

Adding branch with critical sections. Changes to beahviour/schedule.v, new file model/task/critical_sections.v, minor changes in model/processor/multiprocessor.v ideal.v varspeed.v spin.v

This merge request proposes a formalization of critical sections, partially based on ECRTS18 https://prosa.mpi-sws.org/pdf/ecrts18-wip.pdf, in particular for the service-based, temporal characterization, but different insofar as we try to overcome what we perceived as a potential semantic weakness, related to the direct association of sections to jobs independently of any schedule.

Critical sections are generally meant to be sections of code that involve access to resources. When a running job gets to the start of a section, it requests access to the associated resources (at its simplest, just one). In the case of mutually exclusive access, the request may be added to a queue of similar ones, hence the job may be blocked while it waits for its request to be handled. Once the job has ended executing the critical section, it releases the lock.

In our view, there are two main modelling aspects. On one hand, offline, a critical section is part of the code written for a task. Empirically, by testing and cost analysis, it could be associated with relative time bounds, loosely defined with respect to the received service. On the other hand, if and when a critical section is executed, can be generally known only at runtime, and it depends on the actual control flow which might be affected by many factors, including time variables. Of course, runtime absolute time values will be expected to satisfy the task-level relative-time constraints.

The execution of critical sections can be characterized in terms of events such as lock requests and release notifications, initiated by the running job, and access granting issued by the scheduler/lock manager. However, these events can be deduced by simply recording the active lock requests and the locks held for each job.

Therefore we propose to split the representation of critical sections into two layers: on one hand, a loose temporal specification at the task level; on the other hand, information about lock requests and held lock at the level of processor state. The two layers should be related by consistency constraints.

The processor-state layer is implemented as a small extension of the ProcessorState class in behaviour/schedule.v. Together with the lists of the active requests and of the held locks for each job, we add the type of the critical sections as a field, to avoid introducing an extra parameter. The unit type is used as dummy, for the cases in which there are no critical sections. From the refactoring point of view, this extension involves only minor changes to the files in model/processor which contains instantiations of ProcessorState.

The static specification layer is presented in a new file, model/task/critical_sections.v, which depends on the definition of task in concept.v. This specification follows the main lines of the one described in ECRTS18, with some differences.

In fact, we worried that the notion of job, independently of any schedule, might not provide a sufficiently robust basis for the determination of the critical sections that are executed.

In the task-based specification we are proposing, we intend each control flow branch to be associated with a list of sections. We express this implicitly, by associating the task with a list of lists of sections. Consistently with this non-deterministic aspect, we opt for a loose temporal specification: we give earliest start, latest start, minimum length and maximum length of a section, rather than strict start and end points.

The last part of critical_sections.v contains constraints that express critical-section validity of a schedule with respect to a static specification.

Following what appears to be a general approach in Prosa, we use Coq type classes to represent what, in a more concrete, non-extensible representation, could be fields in a record definition. We use Coq definitions to introduce constraints which, from the point of view of our current understanding, should not be normally proven, but only assumed as hypotheses to support higher-level reasoning.

Looking forward to your feedback!