Prosa - Self-Suspending Tasks and Weak Sustainability

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].

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

Then, move to the Prosa directory, generate the Makefile, compile the code and run 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).

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.

    (* We begin by defining the set of possible parameter labels. *)
    Inductive parameter_label :=
      | JOB_ARRIVAL
      | JOB_COST
      | JOB_DEADLINE
      | JOB_JITTER
      | JOB_SUSPENSION.

    (* Next, we associate to each label a type of function over jobs. *)
      Definition type_of_label (l: parameter_label) : Type :=
        match l with
        | JOB_ARRIVAL ⇒ Job → instant
        | JOB_COST ⇒ Job → time
        | JOB_DEADLINE ⇒ Job → time
        | JOB_JITTER ⇒ Job → time
        | JOB_SUSPENSION ⇒ Job → time → duration
      end.

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.

    (* Finally, we define a job parameter as a pair containing a label and a function. *)
    Record job_parameter := param
    {
      p_label : parameter_label;
      p_function : type_of_label p_label
    }.

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}#).

    (* Given a set of labels, we define whether two parameter lists differ only
     by the parameters with those labels.
     Note: This predicate assumes that both lists have similar, unique labels.  *)
     Definition differ_only_by (variable_labels: seq parameter_label) (s1 s2: seq job_parameter) :=
        ∀ (param param': job_parameter),
            List.In param s1 →
            List.In param' s2 →
            p_label param = p_label param' →
            p_label param \notin variable_labels →
            param = param'.

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.

    (* Next, we define whether all jobs sets are schedulable with given params... *)
     Definition jobs_are_schedulable_with (params: seq job_parameter) :=
       ∀ arr_seq sched j,
          belongs_to_task_model params arr_seq sched →
          is_schedulable params sched j.

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.

    (* ...and also define whether all job sets are schedulable with any variation of parameters
     in which the sustainable and variable parameters may change. *)
     Definition jobs_are_V_schedulable_with (params: seq job_parameter) :=
       ∀ (similar_params: seq job_parameter),
          has_consistent_labels similar_params →
          differ_only_by variable_params params similar_params →
          jobs_are_schedulable_with similar_params.

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).

   (* Then, we say that the scheduling policy is weakly-sustainable with sustainable_param
     and variable_params iff the following holds:
        if jobs are V-schedulable with the original parameters, then they are also
        schedulable with better parameters (according to the has_better_params relation). *)
     Definition weakly_sustainable :=
        ∀ (params better_params: seq job_parameter),
            has_consistent_labels params →
            has_consistent_labels better_params →
            differ_only_by [::sustainable_param ] params better_params →
            sustainable_param_becomes_better params better_params →
            jobs_are_V_schedulable_with params →
            jobs_are_schedulable_with better_params.

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.

    (* Also, we say that the scheduling policy is strongly-sustainable
     with sustainable_param iff it is weakly-sustainable with
     sustainable_param and the set of variable parameters is empty. *)
    Definition strongly_sustainable := weakly_sustainable [::].

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.

    (* We define job suspension as a function that takes a job in the arrival
     sequence and its current service and returns how long the job must
     suspend next. *)
    Definition job_suspension := Job →    (* job *)
                                                   time → (* current service *)
                                                   duration. (* duration of next suspension *)

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.

    ( Consider any job suspension function. )
    Variable next_suspension: job_suspension Job.

  ( Next, we define the total suspension time incurred by a job. )
    Definition total_suspension :=
      \sum_(0 ≤ t < job_cost j ) (next_suspension j t).

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

    (* Next, assume that for each task a suspension bound is known. *)
    Variable suspension_bound: Task → duration.

    (* Then, we say that the arrival sequence satisfies the dynamic
       suspension model iff the total suspension time of each job is no
       larger than the suspension bound of its task. *)
    Definition dynamic_suspension_model :=
      ∀ j, total_job_suspension j ≤ suspension_bound (job_task j).

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.

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.

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.

Prosa: Self-Suspending Tasks and Weak Sustainability

Checking the Correctness of the Proofs

Overview of the Specification and Proofs

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

2) Defining the Generic Suspension Model (Section 4.1)

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