In this file, we prove Theorem 1 presented in the paper "What really is pWCET? A Rigorous Axiomatic Definition of pWCET" by Bozhko et al. (RTSS'23).

Step-by-step Proof of Theorem 1

In the following, we present the proof of Theorem 1 in the above-cited paper. Due to the length of the proof and the nature of Coq, we cannot start this section with the statement of the theorem. Instead, we will first prove many "stepping stone" lemmas and then combine them together to obtain a complete proof. Readers who would like to see the final statement of the theorem first are referred to section ProofOfTheorem1.

In this section, we demonstrate a step-by-step proof of the main claim (Theorem 1 from the paper). It is important to note that Coq's preferred method of proof is a "bottom-up" approach, while most humans are prefer following a top-down derivation. In other words, in Coq it is easier to present proofs in the following way: first simple facts are proven, then one can use these simple facts to construct more sophisticated facts, then even more sophisticated ones, and so on until the final goal is reached. Yet, a reasonable question for a human would be "where is this going?" Therefore, we adopt a more paper-like approach in which we present the proof as a series of implications: C → Goal, B → C, A → B. This allows us to begin with the final goal (assuming that some facts are given) and then gradually work our way towards the "leafs" of the overall argument pertaining to specific details. Assume horizon defines (an upper bound on) the termination time of the system. If horizon = None, the system does not necessarily terminate. Note, however, that in either case our proof assumes there to be a finite number of jobs for technical reasons. As the horizon can be chosen to be arbitrarily large (the proof does not depend on its magnitude), e.g., hundreds of even thousands of years, assuming the existence of a finite horizon is not unreasonable for a computing system.

Consider any type of tasks with a notion of pWCET...

...and their jobs.

Consider a response-time monotonic scheduling algorithm ζ, where response-time monotonic means the following: assuming that all arrival times are fixed, an increase of the execution cost of any job cannot cause a decrease in the response time of any job. Recall that ζ receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.

For brevity, let sched denote the probabilistic schedule generated by ζ for a given system S.

As before, consider four parameters that describe a system under analysis: a sample space Ω, a measure μ, job arrival times 𝓐, and job execution costs 𝓒.

Let us use these parameters to construct a system S.

Next, we assume that the aforementioned pWCET is an axiomatic pWCET. That is, for any job j and any arrival sequence ξ, there exists a partition of Ω into positive-probability events such that both partition dominance and partition independence are satisfied.

Suppose we use the construction replace_job_pET presented in probsa/rt/analysis/pETs_to_pWCETs to replace the execution cost of given job j_rep. Let S' denote the resulting system.

For convenience, let tsk denote j's task...

... and let μ_tsk denote the measure induced by pWCET.

Next, consider an arbitrary job j of any task and a duration r.

Finally, let Exc denote the event that j's response time exceeds r time units in system S ...

... and let Exc' denote the event that j's response time exceeds r time units in system S'.

The remainder of this file serves for the most part to relate the probability of Exc with the probability of Exc', namely to establish that ℙ<μ_of S>{[ Exc ]} ≤ ℙ<μ_of S'>{[ Exc' ]}.

Step 1

Now we are ready to start the proof. First, we do a case analysis on all possible arrival sequences.

Consider a partition ξpart of the sample space Ω_of S of system S into events corresponding to different arrival sequences.

Here ξpart is an (indexed) set of events, where an ξi-th event denoted as ξpart◁{ξi} represents a subset of Ω where the arrival sequence is equal to ξi. (Readers focused on technical detail may be interested in noting that the indices of partition ξpart are arrival sequences themselves. This detail may be safely skipped over by more casual readers.) As discussed in the paper, one can transfer the partition ξpart to the system S' and denote it as ξpart'. For further details see the function partition_transfer.extend_partition.

Partitions ξpart and ξpart' are so similar that one can prove equivalence. For example, two indices ξi and ξi' that are "pickle equivalent" can be shown to be identical. (Pickle equivalence is a very strong notion of equivalence; one can intuitively view it simply as an equality between two elements of similar types; for further details see util.bigop_inf.pickle_bij.)

Now, recall that we present the proof in a top-down (C → Goal) fashion, starting with the overall theorem. So, assuming that for any two elements of partitions ξi : I ξpart and ξi' : I ξpart' that are "pickle"-equivalent, it holds that ℙ{[ Exc1 ∩ ξpart◁{ξi} ]} ≤ ℙ{[ Exc2 ∩ ξpart'◁{ξi'} ]}, ...

... we can show that ℙ<μ_of S>{[ Exc1 ]} ≤ ℙ<μ_of S'>{[ Exc2 ]}. Or, in other words, we reduced the lemma statement to the hypothesis statement.

Step 2

Now, we know that if we have the inequality with partitions on arrival sequences H_ineq_ξ_partitioned, then we are done. But how do we prove such an inequality? In the next step, we prove the required inequality by introducing a new hypothesis from which it can be established. We then continue in this manner until reaching a hypothesis that is easy enough to prove without introducing new hypotheses. In the second step, we replace the partition over all arrival sequences with an event encoding one arrival sequence.

First, let us state the premise of our hypothesis H_ineq_ξ_partitioned. Again, consider a partition ξpart of the sample space of system S into events corresponding to different arrival sequences...

... and ξpart to system S' and denote it as ξpart'.

Consider a pair of arbitrary pickle-equivalent elements ξi and ξi'.

As already discussed, pickle-equivalence is quite strong and we can show that both indices ξi and ξi' correspond to the same arrival sequence ξ. Because of the way partitions on arrival sequences are constructed, we can extract an arrival sequence by unpacking a partition.

Instead of clunky indices ξi : I ξpart and ξi' : I ξpart', we will use "plain" predicates ξf and ξf' that correspond to a fixed arrival sequence ξ in S and S', respectively.

During this step, we replace indices with predicates.

Step 3

Now, we can forget about ξpart and ξpart' and use ξ, ξf, and ξf' instead. Notice that here we use ξ to denote the deterministic arrival sequence. Predicates ξf and ξf' denote events that result in ξ in systems S and S', respectively.

Without loss of generality, we can assume that ξ appears with positive probability (otherwise the LHS of the inequality from Step 2 is equal to 0).

In this step, we introduce a partition (that guarantees partition-independence and partition-dominance) of the probability space by exploiting H_axiomatic_pWCET, the assumption of axiomatic pWCET.

Consider some countable type I and define a family of predicates part : I → pred Ω. Consider an index Pi : i and assume that part Pi has positive probability. Note that part might depend on ξf. Next, let us assume the following: we have an event Sf := part Pi in system S such that the event ensures (1) the validity of the pWCET bound and (2) the partition-independence of job j_rep. Let us define Sf's twin Sf' ω := Sf (proj1 ω) in S' (recall that proj1 simply returns the first component of a tuple). With this, let us assume that the inequality that now includes Sf and Sf' holds: ℙ<μ_of S>{[ (Exc1 ∩ ξf) ∩ Sf ]} ≤ ℙ<μ_of S'>{[ (Exc2 ∩ ξf') ∩ Sf' ]} .

Then, we can prove the inequality that we assumed in the previous step (Step2). Notice that in order to apply the conclusion of H_ineq_Ω_part, we need to provide all the premises of the hypothesis. In particular, we have to present a countable type with a family of predicates where every event ensures partition-independence and partition-dominance. This is possible only because we assumed that the given pWCET satisfies our axiomatic pWCET definition. Again, essentially, we prove that we can reduce the lemma to the hypothesis using the properties ensured by axiomatic pWCET.

Step 4

As before, now we need to prove the inequality we assumed in the previous step. For this, let us introduce all premises of the assumed inequality as variables and hypotheses.

In this step, we transform our inequality by moving ξf ∩ Sf and ξf' ∩ Sf' to the conditional part.

First, note that both ξf ∩ Sf and ξf' ∩ Sf' have the same probability. This is due to the fact that our transformation does not change the probabilities of arrival sequences or partitions.

As before, we show that one can reduce the inequality stated in the lemma to the statement stated in the hypothesis. In other words, we can indeed condition on ξf ∩ Sf and ξf' ∩ Sf'. Then, both of them cancel out, since the probability is equal.

Step 5

For simplicity, let us introduce a few local names for functions extracting cost vectors. For example, given ω \in Ω_of S, compute_costs returns a vector of all costs fixed for this specific evolution ω.

For simplicity, let 𝓡 denote a function that computes the response time of any job for given fixed vectors 𝗔 and 𝗖.

In this step, we replace events Exc and Exc' with events λ ω ⇒ exceeds (𝓡 𝗔 (compute_costs ω) j) r, where the arrival times are fixed to be a specific vector of arrival times. Note that previously we had a general random variable describing the response-time distribution, but now we have algorithm 𝓡 instead.

Note that here we assume that we are given any vector 𝗔 describing job arrivals without restriction that it must agree with ξ. Inside of the proof, we indeed construct 𝗔 as a transformation of ξ; however, for further proofs, it is not relevant, so we just forget this information and use a generic function Job → option instant.

The inequality involving Exc and Exc' is implied by the inequality involving 𝓡.

Step 6

Assume that we are given a list of job arrivals.

For technical reasons, we need to distinguish between jobs costs operating in a probabilistic space with a measure μ_of S (μ_of S') and the ones operating with the restricted measure restrict (μ_of S) (ξf ∩ Sf) (and restrict (μ_of S') (ξf' ∩ Sf')). Recall that a partition of the probability space must take measures into account (to satisfy certain assumptions). Since we restrict Ω_of S to a subset that satisfies predicate ξf ∩ Sf (and a subset of Ω_of S' that satisfies predicate ξf' ∩ Sf'), we have to adapt some of the notions to these new measures.

Next, we define random variables, which are the same as those introduced earlier, except for the measure (μr instead of μ and μr' instead of μ'.

Similarly, we need to provide a new notion of projection that accounts for the restricted measure.

Now, we want to fix the job costs of all jobs except j_rep (recall that j_rep is the job for which we want to replace pET with pWCET). For this, again, we introduce partitioning of Ω into subsets, each containing a unique job cost assignment (and the job cost of j_rep is left unspecified).

In the next step, we introduce CSpart◁{Cs} and CSpart'◁{Cs'} into the inequality. They ensure that the costs of all jobs (except j_rep) are fixed.

Assume that the inequality holds when conditioned on job-cost partitions (excluding j_rep), ...

... then we can derive the inequality also without conditioning on costs.

Step 7

As before, we now proceed to derive the premise of the prior step. To this end, consider two equivalent events corresponding to the same setting of job costs in the two systems.

Consider two partitions of Ω_of S and Ω_of S' into cost of all jobs except j_rep.

Similarly to how we replaced job arrivals with 𝗔, we can do a similar trick to replace job costs with a vector 𝗖. However, what do we do with the cost of the unspecified job j_rep? First, we can perform another round of partitioning and apply the law of total Probability (LTP) on the remaining job cost (note that we get a new sum ∑[∞]_{c<-option work} ... in the inequality). Second, we can update 𝗖 with the specified value of j_rep 𝓡 𝗔 (update 𝗖 j_rep c) j. For now, we replace only the LHS.

Note that on the LHS of the below hypothesis, we now have the following term: ∑[∞]_{c<-option work} ℙ<μ_of S>{[ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r && (CSpart◁{Cs} & Cpart◁{c})| ξf ∩ Sf ]}. An important result of this transformation is that now exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r is a boolean value (true/false) and event CSpart◁{Cs} & Cpart◁{c} defines a subset of Ω_of S such that all job costs are fixed. To extract a vector of job costs from the partition CSpart◁{Cs}, we find one ω ∈ CSpart◁{Cs} and compute the vector of costs for this ω. The resulting vector of costs will agree with the jobs in the system, given CSpart◁{Cs} is true. Note that we use the construction update 𝗖 j_rep c to update the cost of job j_rep in vector 𝗖 with a new value c. This is a way to define the notion of "reassembling" two job-cost-fixing vectors used in the paper.

As before, we show that the prior step's premise follows from the hypothesis introduced here; that is, how the premise of Step 6 follows from the premise of Step 7.

Step 8

We can prove that there is at least one ωo that satisfies the current partition CSpart◁{Cs} ωo. We can use ωo to compute 𝗖. Such a cost assignment agrees with CSpart◁{Cs} because ωo satisfies the initial predicate.

Similarly to Step 7, which focused on the LHS, we now replace the RHS.

Notice that both sides now have all costs fully fixed.

From the above hypothesis, we can obtain the premise of Step 7.

Step 9

Let us define a random variable following the pWCET distribution. This random variable describes j_rep's cost after its pET has been replaced. For more details, see the file rt/analysis/pETs_to_pWCETs and specifically the transformation replace_job_pET. Recall that μ_tsk is the measure induced by the given pWCET distribution.

Finally, we can use the independence property H_cond_independence to factorize the LHS. At the same time, we can factorize the RHS just by construction.

On the technical side, this is a pretty involved proof. However, intuitively we simply apply the partition-independence property of Sf. Note that the probability of CSpart◁{Cs} ω && 𝓒 j_rep ω == c factors into two probabilities: CSpart◁{Cs} and 𝓒 j_rep == c.

Next, we show that the probability part of the RHS can be factorized into two terms: ℙ<μ>{[ CSpart◁{Cs} | ξf ∩ Sf]} and ℙ<μ_tsk>{[ fun cω ⇒ Some cω == c ]}. Note that the first factor is no longer a probability with respect to S' --- it is a probability with respect to S. For the second term, it is a probability over the probability space described in the file pETs_to_pWCETs.

As usual, let us state a new premise.

From the preceding factorized inequality, we can derive the premise of the previous step.

Step 10

In this step, we remove ℙ<μ_of S>{[ CSpart◁{Cs} | ξf ∩ Sf ]} on the LHS and ℙ<μ_of S>{[ CSpart◁{Cs} | ξf ∩ Sf' ]} on the RHS.

Let us assume that we can prove the following inequality, where ℙ<μ_of S>{[ CSpart◁{Cs} | ξf ∩ Sf ]} on both sides cancel out, ...

... then we can easily arrive at the preceding step's premise.

Step 11

We have successfully removed constraints on job costs of jobs that are not equal to j_rep. Depending on the cost of j_rep, we can still get different behavior. In this section, we do a case analysis on the "critical" value of the cost of j_rep.

There are three possibilities: (1) whatever cost of job j_rep we pick, the response time of job j never exceeds r, (2) whatever cost of job j_rep we pick, the response time of job j always exceeds r, and (3) there is some critical value c0 such that j's response time will exceed r if and only if j_rep's job cost is larger than r.

Note that case (1) is easy since the inequality reduces to 0 ≤ 0.

Note that case (2) is easy since the inequality reduces to 1 ≤ 1.

Case (3) is interesting; so let us assume that c0 is the critical value, after which the response time of job j will exceed r. However, then I[exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r] can be transformed into c0 ⟨<⟩ c. We use the fancy ⟨<⟩ to account for the fact that both costs can be ⊥.

Given the hypothesis, we can prove the prior step's premise.

Step 12

Let us now assume that there is a cost c0 (of job j_rep) with the property that any cost strictly higher causes j to have a response time larger than r.

Note that ∑_{c} I[c0 < c] ℙ{ X = c } is equivalent to ℙ{X > c0}. We use this property to simplify I[...] on both sides.

Assuming that the following inequality, which is very similar to our initial assumption H_pWCET_bounds_cond_cdf, ...

... we can prove the inequality assumed in the previous step.

Step 13

In the last step, we exploit the top-level assumption H_pWCET_bounds_cond_cdf to finish the proof.

Notice that the following statement is very close to the pWCET guarantee H_pWCET_bounds_cond_cdf.

Also, note that we did not make any new assumptions in this section; hence, we are done.

Statement and Proof of Theorem 1

Now we can combine all the steps to prove that a single job cost can be replaced with the corresponding pWCET while preserving response-time monotonicity (Theorem 1 in the paper).

Assume horizon defines the termination time of the system. If horizon = None, the system does not terminate; however, as discussed at the beginning of the file, we assume a finite number of jobs in either case.

Consider any type of tasks with a notion of pWCET.

Note that the arrivals and costs are determined by the system, which is defined next.

Consider a response-time monotonic scheduling algorithm ζ, where response-time monotonic means the following: assuming that all arrival times are fixed, an increase of the execution cost of any job cannot cause a decrease of the response time of any job. Recall that ζ receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.

Let sched denote a schedule generated by ζ.

Let S be an arbitrary system ...

... and let j_rep be a job whose cost we want to replace.

Let S' be the system where we replace j_rep's cost with the corresponding pWCET via replace_job_pET.

Consider an arbitrary job j ...

... and its response times 𝓡j and 𝓡j' in schedules sched S and sched S', respectively.

If pWCET satisfies our notion of axiomatic pWCET, ...

... then the response-time distribution of job j in schedule sched S is ⪯-bounded by the response-time distribution of job j in schedule sched S'. That is, 𝓡j ⪯ 𝓡j'.