From d0d593eca857ce5d98d34442a3b9f99dbe40bb04 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 18 Nov 2019 14:23:59 +0100
Subject: [PATCH] define dynamic self-suspension model
---
restructuring/model/task/suspension/dynamic.v | 35 +++++++++++++++++++
1 file changed, 35 insertions(+)
create mode 100644 restructuring/model/task/suspension/dynamic.v
diff --git a/restructuring/model/task/suspension/dynamic.v b/restructuring/model/task/suspension/dynamic.v
new file mode 100644
index 000000000..50c3ccd9c
--- /dev/null
+++ b/restructuring/model/task/suspension/dynamic.v
@@ -0,0 +1,35 @@
+Require Export rt.restructuring.model.readiness.suspension.
+Require Export rt.restructuring.model.task.concept.
+
+(** * Task Parameter for the Dynamic Self-Suspension Model *)
+
+(** Under the dynamic self-suspension model, for each task, there is a bound on
+ the maximum total self-suspension duration exhibited by any job of the
+ task. *)
+Class TaskTotalSuspension (Task : TaskType) := task_total_suspension : Task -> duration.
+
+(** * Validity *)
+
+(** In the following section, we specify the semantics of the dynamic
+ self-suspension model: each job self-suspends in total no longer than
+ specified by its associated task. *)
+
+Section ValidDynamicSuspensions.
+
+ (** Consider any kind of jobs,... *)
+ Context {Job : JobType}.
+
+ (** ...where each job has a cost and may exhibit self-suspensions,... *)
+ Context `{JobCost Job} `{JobSuspension Job}.
+
+ (** ...and the tasks from which these jobs stem. *)
+ Context {Task : TaskType}.
+ Context `{JobTask Job Task} `{TaskTotalSuspension Task}.
+
+ (** Under the dynamic self-suspension model, the total self-suspension time
+ of any job cannot exceed the self-suspension bound of its associated
+ task. *)
+ Definition valid_dynamic_suspensions :=
+ forall j, total_suspension j <= task_total_suspension (job_task j).
+
+End ValidDynamicSuspensions.
--
GitLab