Inference of scheduling transformations

From Automated Assistance for Formal Reasoning

This article presents an example that involves reasoning about task scheduling transformations, based on the results in a report on this topic [1].

[edit] Definitions

Assume for any $C, T$ , $(C, T)$ is a task iff $C \in \N$ , $T \in \N$ , $C \geq 1$ , and $T \geq 1$ .

We define a notion of satisfaction for allocations and tasks (sliding window).

Assume for any $a, C, T$ ,

a

satisfies

(C, T)

iff

(C, T)

is a task,

$a \in \{0,1\}^\infty$ , and

for all $m \in \N$ , ${a_m +...+ a_{m+(T-1)}} \geq C$ .

[edit] Results

We prove that for any allocation that satisfies a task, the same allocation satisfies any task with a later

deadline.

Assert for any $a, C, T$ , if $(C, T)$ is a task and $a$ satisfies $(C, T)$ then $T \in \N$ , $T \geq 1$ , $a \in \{0,1\}^\infty$ ,

for all $T' \in \N$ , if $T' \geq T$ then

$(C, T')$ is a task, and

for all $m \in \N$ ,

${a_m +...+ a_{m+(T-1)}} \geq C$ ,

${a_m +...+ a_{m+(T'-1)}} \geq {a_m +...+ a_{m+(T-1)}}$ ,

${a_m +...+ a_{m+(T'-1)}} \geq C$ ,

for all $m \in \N$ , ${a_m +...+ a_{m+(T'-1)}} \geq C$ ,

\l{

a

satisfies

(C, T')

}.

[edit] References

[1] Ishakian, Vatche; Bestavros, Azer; Kfoury, Assaf. A Type-Theoretic Framework for Efficient and Safe Colocation of Periodic Real-time Systems. Technical Report BUCS-TR-2010-002, CS Dept., Boston University, January 24 2010.

Inference of scheduling transformations

From Automated Assistance for Formal Reasoning

[edit] Definitions

[edit] Results

[edit] References

Views

Personal tools

Navigation

Search

Toolbox