Prosa: Self-Suspending Tasks and Weak Sustainability

In the paper On Strong and Weak Sustainability, with an Application to Self-Suspending Tasks, we proposed the notion of weakly-sustainable policy and proved that uniprocessor JLFP scheduling of dynamic self-suspending tasks is weakly-sustainable with respect to job costs and variable suspension times.

To improve the confidence into this result, we present the formalization in Prosa of weak and strong sustainability, the generic suspension model and the main theorem that proves weak sustainability in the context of self-suspending tasks. Moreover, we show how the proofs can be mechanically checked using the built-in tools.

For an introduction to Prosa, we suggest checking out the 2016 Artifact Evaluation. In case of problems or further questions, feel free to ask questions on the mailing list.

Checking the Correctness of the Proofs

We begin by showing how the proofs in Prosa can be checked with the coqchk tool. The easiest way to do it is by running the Virtual Machine (VM) image that we provide, which has all the necessary tools pre-installed: [Download VM Image].

The VM image can be installed by following these instructions.

After booting the virtual machine, open a Terminal window and download Prosa 0.3.

$ cd ~
$ wget
$ unzip

Then, move to the Prosa directory, generate the Makefile, compile the code and run make validate.

$ cd ~/prosa
$ ./
$ make -j4
$ make validate

You should see the following output, confirming that all proofs in Prosa were mechanically checked and do not include any additional Axioms (other than those introduced by the Mathematical Components library).


*Theory: Set is predicative

Overview of the Specification and Proofs

In this section, we give a brief overview of the specification and proofs in Prosa that are related to our work on sustainability. In particular, we present (1) the definitions of weakly- and strongly-sustainable policy, (2) the definition of the suspension model, and (3) the main theorem that proves weak sustainability in the context of self-suspending tasks.

1) Defining Weakly- and Strongly-Sustainable Policy (Sections 2 and 3)

We begin by mapping the sustainability theory discussed in Sections 2 and 3 in the paper to the corresponding definitions in Prosa. For convenience and as a navigation aid, the referenced statements are reproduced here along with links to the original files. Note that the specification can be better understood by reading each file sequentially, as opposed to checking isolated definitions.

To know more about how the Prosa directory is organized, please refer to the table of contents.

 W1) Definition of a job parameter label

[Show code snippet]

Parameter labels associate names to types of job parameters. They are just a technicality that we use to describe the job parameters that arise in the different task models in the literature. Note that new labels can be added as needed.

 W2) Definition of a generic job parameter

[Show code snippet]

This corresponds to Definition 7 in the paper. Each job parameter is represented by a pair that contains a parameter label (e.g., JOB_COST) and the corresponding function (e.g., #f: \mathit{Job} \rightarrow \mathbb{N}#).

 W3) Definition of job sets that only differ by given job parameters

[Show code snippet]

This corresponds to Definition 10 in the paper. The predicate differ_only_by indicates that any pair of corresponding parameters in the two sets params and params' (e.g., job_cost and job_cost') have the same values, except the ones with the labels provided in variable_labels.

 W4) Definition of schedulable job set

[Show code snippet]

This corresponds to Definition 9 in the paper. That is, jobs_are_schedulable_with params indicates that every arrival sequence and every schedule of the assumed task model (and task set) contains no deadline misses.

 W5) Definition of schedulable job set with varying parameters

[Show code snippet]

This corresponds to Definition 21 in the paper. We say that jobs_are_V_schedulable_with params iff jobs are schedulable for every possible variation of the parameters in variable_params (e.g., JOB_SUSPENSION).

 W6) Definition of weakly-sustainable policy

[Show code snippet]

This corresponds to Definition 22 in the paper. We say that the scheduling policy is weakly_sustainable iff whenever the jobs are schedulable with varying variable_params, it must be that the jobs are also schedulable with better sustainable_param. Note that the has_consistent_labels predicate is just a technicality that indicates that the parameters sets do not have garbage labels.

  W7) Definition of strongly-sustainable policy

[Show code snippet]

This corresponds to Definition 23 in the paper. As expected, strongly_sustainable is simply weakly_sustainable instantiated with the empty set of variable labels.

2) Defining the Generic Suspension Model (Section 4.1)

In this section, we define the notion of self-suspension and show how the dynamic suspension model is formalized in Prosa.

 S1) Definition of job suspension times

[Show code snippet]

This corresponds to Definition 26 in the paper. Note that job_suspension allows any suspension pattern to be defined, making it generic and compatible with the existing suspension models.

 S2) Definition of the total suspension time of a job

[Show code snippet]

This corresponds to Definition 27 in the paper and expresses the total suspension time incurred by a job during its lifetime.

 S3) Definition of the dynamic suspension model

[Show code snippet]

This corresponds to Definition 29 in the paper, which denotes the suspension constraint enforced by dynamic self-suspending tasks.

Based on definition S1, we also define a suspended_at predicate that indicates whether a job #j# is suspended at time #t# in a given schedule. The predicate is omitted for simplicity and can be located here.

3) Main Claim of the Weak Sustainability Proof (Section 4.4)

Using the above definition of weak sustainability, we proved in Prosa that uniprocessor JLFP scheduling of dynamic self-suspending tasks is weakly-sustainable with respect to job costs and variable suspension times. In the following, we briefly explain the main claim of this proof, which is located in this file.

First, to be able to refer to job sets of this task model, we defined a predicate that constrains the job parameters, arrival sequence and schedule so that they satisfy the (a) arrival sequence properties, (b) schedule properties, and (c) suspension-related properties.

    ( Then, we define the task model as the combination of such properties. )
    Let belongs_to_task_model (params: seq (job_parameter Job))
                                                 (arr_seq: arrival_sequence Job) (sched: schedule Job) :=
      satisfies_arrival_sequence_properties params arr_seq
      satisfies_schedule_properties params arr_seq sched
      satisfies_suspension_properties params.

The key properties of the predicate are summarized next.

    jobs_come_from_arrival_sequence sched arr_seq
    jobs_must_arrive_to_execute job_arrival sched 
    completed_jobs_dont_execute job_cost sched
    work_conserving job_arrival job_cost job_suspension_duration arr_seq sched
    respects_JLDP_policy job_arrival job_cost job_suspension_duration
    respects_self_suspensions job_arrival job_cost job_suspension_duration sched.
    dynamic_suspension_model job_cost job_task job_suspension_duration task_suspension_bound.

Next, we instantiate the definition of weak sustainability on this task model, using the sustainable parameter job cost and the variable parameter job suspension time.

   Let all_params := [:: JOB_ARRIVAL; JOB_COST; JOB_SUSPENSION].
   Let sustainable_param := JOB_COST.
   Let variable_params := [:: JOB_SUSPENSION].
   Let has_better_sustainable_param (cost cost': Job time) := j, cost j cost' j.

   Let weakly_sustainable_with_job_costs_and_variable_suspension_times :=
      weakly_sustainable all_params response_time_bounded_by_R belongs_to_task_model
                                      sustainable_param has_better_sustainable_param variable_params.

Finally, we prove the main theorem that uniprocessor JLFP scheduling of dynamic self-suspending tasks is weakly-sustainable with respect to job costs and variable suspension times. This corresponds to Theorem 4 in the paper.

  Theorem policy_is_weakly_sustainable:

The theorem follows from the schedule construction described in Section 4.3 in the paper. For more details, see Schedule Construction and Properties of the Generated Schedule in Prosa.