analysis/facts/model/rbf.v

@@ -252,7 +252,7 @@ Section RequestBoundFunctions.
      [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
      that equals 0 for the empty interval delta = 0. *)
   Context `{MaxArrivals Task}.
-  Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
+  Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
   Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
   (** Let's define some local names for clarity. *)

model/task/arrival/arrival_curve_to_rbf.v

+Require Export prosa.util.all.
+Require Export prosa.model.task.arrival.request_bound_functions.
+Require Export prosa.model.task.arrival.curves.
+
+(** * Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF) *)
+
+(** Consider any type of tasks with a given cost ... *)
+Context {Task : TaskType} `{TaskCost Task} `{TaskMinCost Task}.
+
+(**  ... and any type of jobs associated with these tasks. *)
+Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}.
+
+(** In the following, we show a way to convert a given arrival curve, 
+    paired with a worst-case/best-case execution time, to a request-bound function. 
+    Definitions and proofs will handle both lower-bounding and upper-bounding arrival 
+    curves. *)
+Section ArrivalCurveToRBF.
+
+  (** Let [MaxArr] and [MinArr] represent two arrivals curves. [MaxArr] upper-bounds 
+      the possible number or arrivals for a given task, whereas [MinArr] lower-bounds it. *)
+  Context `{MaxArr : MaxArrivals Task} `{MinArr : MinArrivals Task}. 
+
+  (** We define the conversion to a request-bound function as the product of the task cost and the 
+      number of arrivals during [Δ]. In the upper-bounding case, the cost of a task will represent 
+      the WCET of its jobs. Symmetrically, in the lower-bounding case, the cost of a task will 
+      represent the BCET of its jobs. *)
+  Definition task_max_rbf (arrivals :  Task -> duration -> nat) task Δ := task_cost task * arrivals task Δ.
+  Definition task_min_rbf (arrivals :  Task -> duration -> nat) task Δ := task_min_cost task * arrivals task Δ.
+  
+  (** Finally, we show that the newly defined functions are indeed request-bound functions. *)
+  Global Program Instance MaxArrivalsRBF : MaxRequestBound Task := task_max_rbf max_arrivals.
+  Global Program Instance MinArrivalsRBF : MinRequestBound Task := task_min_rbf min_arrivals.
+
+  (** In the following section, we prove that the transformation yields a request-bound 
+      function that conserves correctness properties in both the upper-bounding 
+      and lower-bounding cases. *)     
+  Section Facts.
+
+    (** First, we establish the validity of the transformation for a single, given task. *)
+    Section SingleTask.
+
+      (** Consider an arbitrary task [tsk] ... *)
+      Variable tsk : Task.
+      
+      (** ... and any job arrival sequence. *)
+      Variable arr_seq : arrival_sequence Job.
+
+      (** First, note that any valid upper-bounding arrival curve, after being 
+          converted, is a valid request-bound function. *)
+      Theorem valid_arrival_curve_to_max_rbf:
+        forall (arrivals : Task -> duration -> nat),
+        valid_arrival_curve (arrivals tsk) ->
+        valid_request_bound_function ((task_max_rbf arrivals) tsk).
+      Proof.
+        move => ARR [ZERO MONO].
+        split.
+        - by rewrite /task_max_rbf ZERO muln0.
+        - move => x y LEQ.
+          rewrite /task_max_rbf.
+          destruct (task_cost tsk); first by rewrite mul0n.
+          by rewrite leq_pmul2l //; apply MONO.
+      Qed.
+
+      (** The same idea can be applied in the lower-bounding case. *)
+      Theorem valid_arrival_curve_to_min_rbf:
+        forall (arrivals : Task -> duration -> nat),
+          valid_arrival_curve (arrivals tsk) ->
+          valid_request_bound_function ((task_min_rbf arrivals) tsk).
+      Proof.
+        move => ARR [ZERO MONO].
+        split.
+        - by rewrite /task_min_rbf ZERO muln0.
+        - move => x y LEQ.
+          rewrite /task_min_rbf.
+          destruct (task_min_cost tsk); first by rewrite mul0n.
+          by rewrite leq_pmul2l //; apply MONO.
+      Qed.
+      
+      (** Next, we prove that the task respects the request-bound function in 
+          the upper-bounding case. Note that, for this to work, we assume that the 
+          cost of tasks upper-bounds the cost of the jobs belonging to them (i.e., 
+          the task cost is the worst-case). *)
+      Theorem respects_arrival_curve_to_max_rbf:
+        jobs_have_valid_job_costs ->
+        respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
+        respects_max_request_bound arr_seq tsk ((task_max_rbf MaxArr) tsk).
+      Proof.
+        move=> TASK_COST RESPECT t1 t2 LEQ.
+        specialize (RESPECT t1 t2 LEQ).
+        apply leq_trans with (n := task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
+        - rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
+          rewrite mem_filter => /andP [/eqP TSK _] _.
+          rewrite -TSK.
+          by apply TASK_COST.
+        - by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l.
+      Qed.
+      
+      (** Finally, we prove that the task respects the request-bound function also in 
+          the lower-bounding case. This time, we assume that the cost of tasks lower-bounds 
+          the cost of the jobs belonging to them. (i.e., the task cost is the best-case). *)
+      Theorem respects_arrival_curve_to_min_rbf:
+        jobs_have_valid_min_job_costs ->
+        respects_min_arrivals arr_seq tsk (MinArr tsk) ->
+        respects_min_request_bound arr_seq tsk ((task_min_rbf MinArr) tsk).
+      Proof.
+        move=> TASK_COST RESPECT t1 t2 LEQ.
+        specialize (RESPECT t1 t2 LEQ).
+        apply leq_trans with (n := task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
+        - by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
+        - rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
+          rewrite mem_filter => /andP [/eqP TSK _] _.
+          rewrite -TSK.
+          by apply TASK_COST.
+      Qed.
+      
+    End SingleTask.
+
+    (** Next, we lift the results to the previous section to an arbitrary task set. *)
+    Section TaskSet.
+      
+      (** Let [ts] be an arbitrary task set... *)
+      Variable ts : TaskSet Task.
+      
+      (** ... and consider any job arrival sequence. *)
+      Variable arr_seq : arrival_sequence Job.
+
+      (** First, we generalize the validity of the transformation to a task set both in
+          the upper-bounding case ... *)
+      Corollary valid_taskset_arrival_curve_to_max_rbf:
+        valid_taskset_arrival_curve ts MaxArr ->
+        valid_taskset_request_bound_function ts MaxArrivalsRBF.
+      Proof.
+        move=> VALID tsk IN.
+        specialize (VALID tsk IN).
+        by apply valid_arrival_curve_to_max_rbf.
+      Qed.
+      
+      (** ... and in the lower-bounding case. *)
+      Corollary valid_taskset_arrival_curve_to_min_rbf:
+        valid_taskset_arrival_curve ts MinArr ->
+        valid_taskset_request_bound_function ts MinArrivalsRBF.
+      Proof.
+        move=> VALID tsk IN.
+        specialize (VALID tsk IN).
+        by apply valid_arrival_curve_to_min_rbf.
+      Qed.
+      
+      (** Second, we show that a task set that respects a given arrival curve also respects 
+          the produced request-bound function, lifting the result obtained in the single-task 
+          case. The result is valid in the upper-bounding case... *) 
+      Corollary taskset_respects_arrival_curve_to_max_rbf:
+        jobs_have_valid_job_costs ->
+        taskset_respects_max_arrivals arr_seq ts ->
+        taskset_respects_max_request_bound arr_seq ts.
+      Proof.
+        move=> TASK_COST SET_RESPECTS tsk IN.
+        by apply respects_arrival_curve_to_max_rbf, SET_RESPECTS.
+      Qed.
+      
+      (** ...as well as in the lower-bounding case. *)
+      Corollary taskset_respects_arrival_curve_to_min_rbf:
+        jobs_have_valid_min_job_costs ->
+        taskset_respects_min_arrivals arr_seq ts ->
+        taskset_respects_min_request_bound arr_seq ts.
+      Proof.
+        move=> TASK_COST SET_RESPECTS tsk IN.
+        by apply respects_arrival_curve_to_min_rbf, SET_RESPECTS.
+      Qed.
+      
+    End TaskSet.
+
+  End Facts.
+  
+End ArrivalCurveToRBF.

model/task/arrival/curves.v

@@ -60,7 +60,7 @@ Section ArrivalCurves.
     (** We say that a given curve [num_arrivals] is a valid arrival curve for
         task [tsk] iff [num_arrivals] is a monotonic function that equals 0 for
         the empty interval [delta = 0]. *)
-    Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration -> nat) :=
+    Definition valid_arrival_curve (num_arrivals : duration -> nat) :=
       num_arrivals 0 = 0 /\
       monotone num_arrivals leq.
 
@@ -134,7 +134,7 @@ Section ArrivalCurvesModel.
   (** We say that [arrivals] is a valid arrival curve for a task set
       if it is valid for any task in the task set *)
   Definition valid_taskset_arrival_curve (arrivals : Task -> duration -> nat) :=
-    forall (tsk : Task), tsk \in ts -> valid_arrival_curve tsk (arrivals tsk).
+    forall (tsk : Task), tsk \in ts -> valid_arrival_curve (arrivals tsk).
 
   (** Finally, we lift the per-task semantics of the respective arrival and
   separation curves to the entire task set.  *)

model/task/arrivals.v

@@ -43,7 +43,7 @@ Section TaskArrivals.
 
   (** ... and also count the cost of job arrivals. *)
   Definition cost_of_task_arrivals (t1 t2 : instant) :=
-    \sum_(j <- task_arrivals_between t1 t2 | job_task j == tsk) job_cost j.
+    \sum_(j <- task_arrivals_between t1 t2) job_cost j.
 
 End TaskArrivals.
 

model/task/concept.v

@@ -26,6 +26,10 @@ Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
     execution cost (WCET). *)
 Class TaskCost (Task : TaskType) := task_cost : Task -> duration.
 
+(** And finally, we define a task-model parameter to express each task's best-case
+    execution cost (BCET). *)
+Class TaskMinCost (Task : TaskType) := task_min_cost : Task -> duration.
+
 
 (** * Task Model Validity *)
 
@@ -33,9 +37,10 @@ Class TaskCost (Task : TaskType) := task_cost : Task -> duration.
     model must satisfy. *)
 Section ModelValidity.
 
-  (** Consider any type of tasks with WCETs and relative deadlines. *)
+  (** Consider any type of tasks with WCETs/BCETs and relative deadlines. *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
+  Context `{TaskMinCost Task}.
   Context `{TaskDeadline Task}.
 
   (** First, we constrain the possible WCET values of a valid task. *)
@@ -67,7 +72,11 @@ Section ModelValidity.
     Definition valid_job_cost j :=
       job_cost j <= task_cost (job_task j).
 
-    (** ... and any arrival sequence. *)
+    (** Every job have a valid job cost *)
+    Definition jobs_have_valid_job_costs :=
+      forall j, valid_job_cost j.
+
+    (** Next, consider any arrival sequence. *)
     Variable arr_seq : arrival_sequence Job.
 
     (** The cost of a job from the arrival sequence cannot
@@ -78,6 +87,36 @@ Section ModelValidity.
         valid_job_cost j.
 
   End ValidJobCost.
+  
+  (** Third, we relate the cost of a task's jobs to its BCET. *)
+  Section ValidMinJobCost.
+
+    (** Consider any type of jobs associated with the tasks ... *)
+    Context {Job : JobType}.
+    Context `{JobTask Job Task}.
+    (** ... and consider the cost of each job. *)
+    Context `{JobCost Job}.
+
+    (** The cost of any job [j] cannot be less than the BCET of its respective
+        task. *)
+    Definition valid_min_job_cost j :=
+      task_min_cost (job_task j) <= job_cost j.
+    
+    (** Every job have a valid job cost *)
+    Definition jobs_have_valid_min_job_costs :=
+      forall j, valid_min_job_cost j.
+
+    (** Next, consider any arrival sequence. *)
+    Variable arr_seq : arrival_sequence Job.
+
+    (** The cost of a job from the arrival sequence cannot
+       be less than the task cost. *)
+    Definition arrivals_have_valid_min_job_costs :=
+      forall j,
+        arrives_in arr_seq j ->
+        valid_min_job_cost j.
+
+  End ValidMinJobCost.
 
 End ModelValidity.
 

scripts/record-proof-state.py

@@ -27,6 +27,7 @@ import argparse
 import sys
 import os
 import re
+import time
 from subprocess import Popen, PIPE
 from select import select
 
@@ -56,6 +57,12 @@ def statement_end_offsets(opts, src):
         else:
             return False
 
+    def prev_is(i, c):
+        if i > 0:
+            return src[i - 1] == c
+        else:
+            return False
+
     def next_is_whitespace(i):
         if i + 1 < len(src):
             return src[i + 1].isspace()
@@ -140,10 +147,15 @@ def statement_end_offsets(opts, src):
         # look for closing braces -- this is a brittle heuristic, but
         # we need to catch sub-proofs because coqtop in emacs mode
         # produces a prompt every time we enter a sub-proof
-        elif not in_comment and in_proof and cur_is(i, '}') \
-             and next_is_whitespace(i) and prev_is_whitespace(i):
-            yield i + 1
-            last = i + 1
+        elif not in_comment and in_proof and cur_is(i, '}') and \
+             (next_is_whitespace(i) or next_is (i, '}')) and \
+             (prev_is_whitespace(i) or prev_is(i, '}')):
+            if next_is_whitespace(i):
+                yield i + 1
+                last = i + 1
+            else:
+                yield i
+                last = i
         # similarly, look for opening braces
         elif not in_comment and in_proof and cur_is(i, '{') \
              and next_is_whitespace(i) and prev_is_whitespace(i):
@@ -198,6 +210,8 @@ def read_from_pipe(pipe, timeout, seen_enough = lambda _: False, expect_timeout=
                 output += data
     return output.decode("utf-8")
 
+COQ_PROMPT_RE = re.compile(r"<prompt>\S* < ([0-9]+) ")
+
 def wait_for_prompt(opts, pipe, timeout):
     seen_enough = lambda output: output.endswith(END_OF_PROMPT_BYTES)
     output = read_from_pipe(pipe, timeout, seen_enough)
@@ -206,18 +220,23 @@ def wait_for_prompt(opts, pipe, timeout):
         more = read_from_pipe(pipe, 0, seen_enough, expect_timeout=True)
         output += more
         if more:
-            print("unexpected:", more)
+            print("Unexpected coqtop output:", more)
             assert False # we lost sync; this should not be happening
         else:
             break
 
+    # check for interaction number in output
+    m = COQ_PROMPT_RE.search(output)
+    prompt_number = int(m.group(1)) if m else -1
     # remove any prompts; we don't want to record those
     if output.endswith(END_OF_PROMPT) and not opts.verbose:
         idx = output.find(START_OF_PROMPT)
-        assert not START_OF_PROMPT in output[:idx] # only one prompt expected
-        return output[:idx]
+        if START_OF_PROMPT in output[idx+1:]:
+            print("Unexpected number of prompts in coqtop output: \n", output)
+            assert False # only one prompt expected
+        return (prompt_number, output[:idx])
     else:
-        return output
+        return (prompt_number, output)
 
 INFO_MSG_PATTERN = re.compile(
 r"""
@@ -235,7 +254,7 @@ def extract_info_messages(output):
 
 def wait_for_coqtop(opts, coqtop):
     # wait until prompt (re-)appears
-    error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
+    num, error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
     # read output produced so far
     # FIXME: this only works if all output fits into the OS's pipe buffer
     output = read_from_pipe(coqtop.stdout, 0)
@@ -246,6 +265,8 @@ def wait_for_coqtop(opts, coqtop):
     error  = error.rstrip()
     if error:
         interaction['error'] = error
+    if num >= 0:
+        interaction['prompt_number'] = num
     return interaction
 
 def interact(opts, coqtop, src, start, end):
@@ -255,7 +276,7 @@ def interact(opts, coqtop, src, start, end):
     coqtop.stdin.write(bytes(input.replace('\n', ' ') + '\n', "utf-8"))
     coqtop.stdin.flush()
     # wait until prompt (re-)appears
-    error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
+    num, error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
     # read output produced so far
     # FIXME: this only works if all output fits into the OS's pipe buffer
     output = read_from_pipe(coqtop.stdout, 0)
@@ -280,6 +301,9 @@ def interact(opts, coqtop, src, start, end):
     if error:
         interaction['error'] = error
 
+    if num >= 0:
+        interaction['prompt_number'] = num
+
     return interaction
 
 def report(n, interaction):
@@ -294,6 +318,38 @@ def report(n, interaction):
         print("PROMPT: [%s]" % interaction['error'].strip())
     print("-" * 80)
 
+
+def prompt_out_of_sync(opts, input_number, interaction):
+    if 'prompt_number' in interaction:
+        if interaction['prompt_number'] != input_number:
+            print("[%s] Out of sync: prompt %d in response to input %d" %
+                   (opts.fname, interaction['prompt_number'], input_number))
+            return True
+    return False
+
+def output_out_of_sync(opts, cmd, interactions):
+    if cmd == 'Qed.':
+        # QED: there should be no more proof obligations.
+        if 'output' in interactions[-2] and \
+           interactions[-2]['output'] != ['No more subgoals.']:
+            print("[%s] Out of sync: 'Qed.' before 'No more subgoals.'" % opts.fname)
+            return True
+        # QED: there should be no output.
+        if 'output' in interactions[-1]:
+            print("[%s] Out of sync: 'Qed.' produced output.'"  % opts.fname)
+            return True
+    elif cmd.startswith('End '):
+        # End of section.
+        if 'output' in interactions[-1]:
+            print("[%s] Out of sync: 'End' produced output.'"  % opts.fname)
+            return True
+    return False
+
+
+# Some vernacular commands that we need to check for because they change
+# coqtop's prompt counter. This list is likely incomplete.
+VERNACULAR_COMMANDS_RE = re.compile(r"(Opaque|Transparent) \S+\.")
+
 def feed_to_coqtop(opts, src):
     coqtop = launch_coqtop(opts)
     interactions = []
@@ -304,14 +360,29 @@ def feed_to_coqtop(opts, src):
         report(0, interaction)
     interactions.append(interaction)
 
+    coq_prompt_offset = 0
+
     # feed statements
     last = 0
     for end in statement_end_offsets(opts, src):
+        if opts.pause:
+            time.sleep(0.1)
+        cmd = src[last:end+1].strip()
+        if VERNACULAR_COMMANDS_RE.match(cmd):
+            coq_prompt_offset += 1
         interaction = interact(opts, coqtop, src, last, end)
         interactions.append(interaction)
         last = end + 1
-        if opts.verbose:
-            report(len(interactions), interaction)
+
+        sync_failure = False
+        sync_failure |= prompt_out_of_sync(opts, len(interactions) + coq_prompt_offset, interaction)
+        sync_failure |= output_out_of_sync(opts, cmd, interactions)
+
+        if opts.verbose or sync_failure:
+            report(len(interactions) + coq_prompt_offset, interaction)
+
+        assert not sync_failure
+
 
     # signal end of input
     coqtop.stdin.close()
@@ -332,6 +403,7 @@ def feed_to_coqtop(opts, src):
 
 def process(opts, fname):
     print("Collecting proof state for %s..." % fname)
+    opts.fname = fname
     src = open(fname, 'r').read()
     interactions = feed_to_coqtop(opts, src)
     ext = '.proofstate.yaml' if opts.yaml else '.proofstate.json'
@@ -383,6 +455,9 @@ def parse_args():
     parser.add_argument('--verbose', default=False, action='store_true',
                         help='report on interaction with coqtop')
 
+    parser.add_argument('--pause', default=False, action='store_true',
+                        help='pause briefly before feeding data to coqtop')
+
     parser.add_argument('--parse-only', default=False, action='store_true',
                         help='report how the script splits the input '
                              '(--verbose for per-character info)')

scripts/wordlist.pws

@@ -38,6 +38,8 @@ RBF
 RBFs
 WCET
 WCETs
+BCET
+BCETs
 Layland
 Liu
 sequentiality