1. Toshimi Sawada Avatar Toshimi Sawada
  2. Untitled project
  3. CafeOBJ

Wiki

Clone wiki

CafeOBJ / OSEK / contents / index-e / backup / 11_Basis_of_TaskScheduling

View History

Basis of Task Scheduling in the OSEK OS

In this section, we introduce the base structure of the OSEK OS where the deadlock freeness is guaranteed. The priority inversion freeness is also guaranteed if rescheduling is properly carried out at every reschedulable point.

PRIORITY

#!python
module PRIORITY
{
  imports
  {
    pr(ENTITY)
    ex(OBSERVER2NUMBER)
  }
  signature
  {
    op priority : Entity -> Observer2Number
  }
}

PRIOR

#!python
module PRIOR
{
  imports
  {
    pr(COMPARISON)
    pr(PRIORITY)
    ex(OBSERVER2RELATION/ENTITY)
  }
  signature
  {
    op prior : -> Observer2Relation/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  (X prior(S) Y) = (priority(X)(S) > priority(Y)(S)) .
    eq deducible((X prior(S) Y) |- (priority(X)(S) > priority(Y)(S))) = true .
    eq deducible((priority(X)(S) > priority(Y)(S)) |- (X prior(S) Y)) = true .
  }
}

For any S : System, the relation prior(S) is irreflexive, asymmetric and transitive. So it can be regarded as a partial order.

#!python
module CLAIM1/PRIOR
{
  imports
  {
    pr(LK)
    pr(PRIOR)
  }
  signature
  {
    op s : -> System
    ops x y z : -> Entity
    ops claim1 claim2 claim3 : -> Prop
  }
  axioms
  {
    eq claim1 = deducible((x prior(s) x) |- nil) . 
    eq claim2 = deducible((x prior(s) y),(y prior(s) x) |- nil) . 
    eq claim3 = deducible((x prior(s) y),(y prior(s) z) |- (x prior(s) z)) . 
  }
}
The proof scores to confiem irreflexivity, asymmetricity and transitivity of prior(s) are listed below.

#!python
-- confirm irreflexivity
open CLAIM1/PRIOR .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((priority(x)(s) > priority(x)(s)) |- nil) .
eq q2 = ((x prior(s) x) |- (priority(x)(s) > priority(x)(s))) .
eq antecedent(i) = (q1,q2) .
eq ((x prior(s) x) |- nil) = consequent(i) .
red claim1 .
close

-- confirm asymmetricity
open CLAIM1/PRIOR .
ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((priority(x)(s) > priority(y)(s)),(priority(y)(s) > priority(x)(s)) |- nil) .
eq q2 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q3 = ((y prior(s) x) |- (priority(y)(s) > priority(x)(s))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x prior(s) y),(y prior(s) x) |- nil) = consequent(i) .
red claim2 .
close

-- confirm transitivity
open CLAIM1/PRIOR .
ops i1 i2 : -> Inference .
ops q1 q2 q3 q4 : -> Sequent .
eq q1 = ((priority(x)(s) > priority(y)(s)),(priority(y)(s) > priority(z)(s))
         |- (priority(x)(s) > priority(z)(s))) .
eq q2 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q3 = ((y prior(s) z) |- (priority(y)(s) > priority(z)(s))) .
eq q4 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x prior(s) y),(y prior(s) z) |- (priority(x)(s) > priority(z)(s))) => consequent(i1) .
trans consequent(i1) => ((x prior(s) y),(y prior(s) z) |- (priority(x)(s) > priority(z)(s))) .
eq antecedent(i2) = (consequent(i1),q4) .
eq ((x prior(s) y),(y prior(s) z) |- (x prior(s) z)) = consequent(i2) .
red claim3 .
THe following is the result of executing the above scores. All claims, i.e., claim1, claim2 and claim3 are reduced to true.

#!python
-- reduce in %CLAIM1/PRIOR : (claim1):Prop

** Found [state 3] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 30 rewrites(0.010 sec), 219 matches, 1 memo hits)

%CLAIM1/PRIOR> red claim2 .
-- reduce in %CLAIM1/PRIOR : (claim2):Prop

** Found [state 378] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 2766 rewrites(1.840 sec), 94754 matches, 1384 memo hits)

 %CLAIM1/PRIOR> *
-- reduce in %CLAIM1/PRIOR : (claim3):Prop

** Found [state 11] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 5928] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 43251 rewrites(40.360 sec), 1646045 matches, 23605 memo hits)
Furthermore, the relation prior(s) satisfies the following condition listed in the module LEMMA5/COMPLEMENT.

For any X,Y,Z : Elt and S : System,

  • deducible((X [prior(S)] Y),(Y prior(S) Z) |- (X prior(S) Z)) = true

  • deducible((X prior(S) Y),(Y [prior(S)] Z) |- (X prior(S) Z)) = true

  • deducible((X [prior(S)] Y),(Y [prior(S)] Z) |- (X [prior(S)] Z)) = true

To confirm these conditions are true, we need to instantiate LEMMA5/COMPLEMENT.

#!python
make LEMMA1/PRIORITY
(
  LEMMA5/COMPLEMENT(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number },
    IRREFLEXIVE/NUMBER { sort Irreflexive -> Irreflexive/Number },
    ASYMMETRIC/NUMBER { sort Asymmetric -> Asymmetric/Number },
    TRANSITIVE/NUMBER { sort Transitive -> Transitive/Number },
    PARTIALORDER/NUMBER { sort PartialOrder -> PartialOrder/Number },
    TOTALORDER/NUMBER { sort TotalOrder -> TotalOrder/Number },
    COMPLEMENT/NUMBER
  )
)

#!python
open PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY .
ops s : -> System .
ops x y z : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x [prior(s)] y),(y prior(s) z) |- (x prior(s) z)) .
ops i1 : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (priority(x)(s) [>] priority(y)(s)),(priority(y)(s) > priority(x)(s))) .
eq q2 = ((priority(y)(s) > priority(x)(s)) |- (y prior(s) x)) .
eq q3 = ((x [prior(s)] y),(y prior(s) x) |- nil) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) => consequent(i1) .
trans consequent(i1) => ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) .
ops i2 : -> Inference .
ops q4 q5 q6 : -> Sequent .
eq q4 = ((priority(x)(s) [>] priority(y)(s)),
         (priority(y)(s) > priority(z)(s))
         |- (priority(x)(s) > priority(z)(s))) .
eq q5 = ((y prior(s) z) |- (priority(y)(s) > priority(z)(s))) .
eq q6 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) .
eq antecedent(i2) = (q4,q5,q6) .
trans ((priority(x)(s) [>] priority(y)(s)),(y prior(s) z) |- (x prior(s) z)) => consequent(i2) .
trans consequent(i2) => ((priority(x)(s) [>] priority(y)(s)),(y prior(s) z) |- (x prior(s) z)) .
ops i3 : -> Inference .
eq antecedent(i3) = (consequent(i1),consequent(i2)) .
eq ((x [prior(s)] y),(y prior(s) z) |- (x prior(s) z)) = consequent(i3) .
red claim .
close

#!python
%PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY> red claim .
*
-- reduce in %PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY : 
    (claim):Prop

** Found [state 26] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 7790] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1201] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 47046 rewrites(53.790 sec), 1807125 matches, 25521 memo hits)


#!python
open PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY .
ops s : -> System .
ops x y z : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x prior(s) y),(y [prior(s)] z) |- (x prior(s) z)) .
ops i1 : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (priority(y)(s) [>] priority(z)(s)),(priority(z)(s) > priority(y)(s))) .
eq q2 = ((priority(z)(s) > priority(y)(s)) |- (z prior(s) y)) .
eq q3 = ((y [prior(s)] z),(z prior(s) y) |- nil) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) => consequent(i1) .
trans consequent(i1) => ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) .
ops i2 : -> Inference .
ops q4 q5 q6 : -> Sequent .
eq q4 = ((priority(x)(s) > priority(y)(s)),
         (priority(y)(s) [>] priority(z)(s))
         |- (priority(x)(s) > priority(z)(s))) .
eq q5 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q6 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) .
eq antecedent(i2) = (q4,q5,q6) .
trans ((x prior(s) y),(priority(y)(s) [>] priority(z)(s)) |- (x prior(s) z)) => consequent(i2) .
trans consequent(i2) => ((x prior(s) y),(priority(y)(s) [>] priority(z)(s)) |- (x prior(s) z)) .
ops i3 : -> Inference .
eq antecedent(i3) = (consequent(i1),consequent(i2)) .
eq ((x prior(s) y),(y [prior(s)] z) |- (x prior(s) z)) = consequent(i3) .
red claim .
close

#!python
%PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY> *
-- reduce in %PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY : 
    (claim):Prop

** Found [state 26] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 8492] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1201] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 47046 rewrites(54.590 sec), 1817930 matches, 25521 memo hits)

#!python
open PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY .
ops s : -> System .
ops x y z : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x [prior(s)] y),(y [prior(s)] z) |- (x [prior(s)] z)) .
ops i1 : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (priority(x)(s) [>] priority(y)(s)),(priority(y)(s) > priority(x)(s))) .
eq q2 = ((priority(y)(s) > priority(x)(s)) |- (y prior(s) x)) .
eq q3 = ((x [prior(s)] y),(y prior(s) x) |- nil) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) => consequent(i1) .
trans consequent(i1) => ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) .
ops i2 : -> Inference .
ops q4 q5 q6 : -> Sequent .
eq q4 = (nil |- (priority(y)(s) [>] priority(z)(s)),(priority(z)(s) > priority(y)(s))) .
eq q5 = ((priority(z)(s) > priority(y)(s)) |- (z prior(s) y)) .
eq q6 = ((y [prior(s)] z),(z prior(s) y) |- nil) .
eq antecedent(i2) = (q4,q5,q6) .
trans ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) => consequent(i2) .
trans consequent(i2) => ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) .
ops i3 : -> Inference .
ops q7 q8 q9 : -> Sequent .
eq q7 = ((priority(x)(s) [>] priority(z)(s)),(priority(z)(s) > priority(x)(s)) |- nil) .
eq q8 = ((z prior(s) x) |- (priority(z)(s) > priority(x)(s))) .
eq q9 = (nil |- (x [prior(s)] z),(z prior(s) x)) .
eq antecedent(i3) = (q7,q8,q9) .
trans ((priority(x)(s) [>] priority(z)(s)) |- (x [prior(s)] z)) => consequent(i3) .
trans consequent(i3) => ((priority(x)(s) [>] priority(z)(s)) |- (x [prior(s)] z)) .
ops i4 : -> Inference .
ops q10 : -> Sequent .
eq q10 = ((priority(x)(s) [>] priority(y)(s)),
          (priority(y)(s) [>] priority(z)(s))
          |- (priority(x)(s) [>] priority(z)(s))) .
eq antecedent(i4) = (q10,consequent(i1),consequent(i2)) .
trans ((x [prior(s)] y),(y [prior(s)] z) |- (priority(x)(s) [>] priority(z)(s))) => consequent(i4) .
trans consequent(i4) => ((x [prior(s)] y),(y [prior(s)] z) |- (priority(x)(s) [>] priority(z)(s))) .
ops i5 : -> Inference .
eq antecedent(i5) = (consequent(i3),consequent(i4)) .
eq ((x [prior(s)] y),(y [prior(s)] z) |- (x [prior(s)] z)) = consequent(i5) .
red claim .
close

#!python
%PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY> *
-- reduce in %PRIOR + LEMMA1/PRIORITY + COMPLEMENT/ENTITY : 
    (claim):Prop

** Found [state 26] (consequent(i5)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 6012] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1201] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1201] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1203] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 30409 rewrites(34.270 sec), 1074588 matches, 16382 memo hits)

PRIOR (redifined)

#!python
module PRIOR
{
  imports
  {
    pr(COMPARISON)
    pr(PRIORITY)
    ex(OBSERVER2PARTIALORDER'/ENTITY)
  }
  signature
  {
    op prior : -> Observer2PartialOrder'/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  (X prior(S) Y) = (priority(X)(S) > priority(Y)(S)) .
    eq deducible((X prior(S) Y) |- (priority(X)(S) > priority(Y)(S))) = true .
    eq deducible((priority(X)(S) > priority(Y)(S)) |- (X prior(S) Y)) = true .
  }
}

ENTRY

#!python
module ENTRY
{
  imports
  {
    pr(OBSERVER2LIST/ENTITY)
  }
  signature
  {
    op entry : -> Observer2List/Entity
  }
}

RUNNABLE

#!python
module RUNNABLE
{
  imports
  {
    ex(OBSERVER2SET/ENTITY)
  }
  signature
  {
    op runnable : -> Observer2Set/Entity
  }
}

AHEAD

#!python
module AHEAD
{
  imports
  {
    pr(FORMER/ENTITY)
    pr(ENTRY)
    ex(OBSERVER2RELATION/ENTITY)
  }
  signature
  {
    op ahead : -> Observer2Relation/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
    eq (X ahead(S) Y) = (X former(entry(S)) Y) .
  }
}

#!python
open AHEAD .
ops s : -> System .
ops x y z : -> Entity .
red deducible((x ahead(s) x) |- nil) .
red deducible((x ahead(s) y),(y ahead(s) x) |- nil) .
red deducible((x ahead(s) y),(y ahead(s) z) |- (x ahead(s) z)) .
close

#!python
-- opening module AHEAD.. done.
%AHEAD> %AHEAD> %AHEAD> _*
-- reduce in %AHEAD : (deducible(((x (ahead s) x) |- nil))):Prop
(true):Bool
(0.000 sec for parse, 2 rewrites(0.000 sec), 7 matches)
%AHEAD> -- reduce in %AHEAD : (deducible((((x (ahead s) y) , (y (ahead s) x)) |- nil))):Prop
(true):Bool
(0.000 sec for parse, 3 rewrites(0.000 sec), 17 matches)
%AHEAD> -- reduce in %AHEAD : (deducible((((x (ahead s) y) , (y (ahead s) z)) |- (x (ahead s) z)))):Prop
(true):Bool
(0.000 sec for parse, 4 rewrites(0.000 sec), 19 matches)

AHEAD (redefined)

#!python
module AHEAD
{
  imports
  {
    pr(FORMER/ENTITY)
    pr(ENTRY)
    ex(OBSERVER2PARTIALORDER/ENTITY)
  }
  signature
  {
    op ahead : -> Observer2PartialOrder/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  (X ahead(S) Y) = (X former(entry(S)) Y) .
    eq deducible((X former(entry(S)) Y) |- (X ahead(S) Y)) = true .
    eq deducible((X ahead(S) Y) |- (X former(entry(S)) Y)) = true .
    eq deducible((X ? entry(S)),(Y ? entry(S)) |- (X ahead(S) Y),(X = Y),(Y ahead(S) X)) = true .
  }
}

PRECEDE

#!python
module PRECEDE
{
  imports
  {
    pr(PRIOR)
    pr(AHEAD)
    pr(COMBINE/ENTITY)
  }
  signature
  {
    op precede : -> Observer2PartialOrder/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  eq precede(S) = [prior(S);ahead(S)] .
    eq deducible((X precede(S) Y) |- (X [prior(S);ahead(S)] Y)) = true .
    eq deducible((X [prior(S);ahead(S)] Y) |- (X precede(S) Y)) = true .
  }
}

NEXT

#!python
module NEXT
{
  imports
  {
    pr(ROOT/ENTITY)
    pr(PRECEDE)
    ex(RUNNABLE)
  }
  signature
  {
    op next : -> Observer2Set/Entity
  }
  axioms
  {
    vars S : System
    vars X : Entity
--  eq next(S) = root(runnable(S),precede(S)) .
    eq deducible((X @ next(S)) |- (X @ root(runnable(S),precede(S)))) = true .
    eq deducible((X @ root(runnable(S),precede(S))) |- (X @ next(S))) = true .
  }
}

CURRENT

#!python
module CURRENT
{
  imports
  {
    ex(OBSERVER2SET/ENTITY)
  }
  signature
  {
    op current : -> Observer2Set/Entity
  }
}

EXECUTED

#!python
module EXECUTED
{
  imports
  {
    ex(OBSERVER2SET/ENTITY)
  }
  signature
  {
    op executed : -> Observer2Set/Entity
  }
}

BLOCK

#!python
module BLOCK
{
  imports
  {
    ex(OBSERVER2RELATION/ENTITY)
  }
  signature
  {
    op block : -> Observer2Relation/Entity
  }
}

STATE

#!python
module STATE
{
  imports
  {
    pr(ASSIGN)
    pr(CURRENT)
    pr(RUNNABLE)
    pr(EXECUTED)
    pr(PRECEDE)
    pr(BLOCK)
  }
}

THEOREM

Suppose that for all X,Y : Entity and S : System, the following sequents can be deducible:

  • ((X ∈ executed(S)),(Y ahead(S) X) |- (X prior(S) Y))

  • ((X ∈ current(S)),(X ahead(S) Y),(Y ∈ executed(S)) |- nil)

  • ((X block(S) Y),(X ahead(S) Y),(Y ∈ executed(S)) |- nil)

  • ((X block(S) Y) |- (X ∈ executed(S)))

  • ((X ∈ runnable(S)) |- (X ∈ entry(S)))

  • ((X block(S) X) |- nil)

  • (nil |- (X ∈ executed(S)),(priority(X)(S) = assign(X)))

  • ((X block(S) Y),(assign(Y) > priority(X)(S)) |- nil)

Then, if X and Y are included in runnable(S), the next sequent can be also deducible.

  • ((X block(S) Y) |- (X precede(S) Y))

#!python
open STATE + LK .

-- hypothesis of the theorem:
vars S : System .
vars X Y : Entity .

eq deducible((X @ executed(S)),(Y ahead(S) X) |- (X prior(S) Y)) = true .
eq deducible((X @ current(S)),(X ahead(S) Y),(Y @ executed(S)) |- nil) = true .
eq deducible((X block(S) Y),(X ahead(S) Y),(Y @ executed(S)) |- nil) = true .
eq deducible((X block(S) Y) |- (X @ executed(S))) = true .
eq deducible((X @ runnable(S)) |- (X ? entry(S))) = true .
eq deducible((X block(S) X) |- nil) = true .
eq deducible(nil |- (X @ executed(S)),(priority(X)(S) = assign(X))) = true .
eq deducible((X block(S) Y),(assign(Y) > priority(X)(S)) |- nil) = true .

ops s : -> System .
ops x y : -> Entity .
eq deducible(nil |- (x @ runnable(s))) = true .
eq deducible(nil |- (y @ runnable(s))) = true .
ops claim : -> Prop .
eq claim = deducible((x block(s) y) |- (x precede(s) y)) .

ops q11 q12 q13 : -> Sequent .
eq q11 = ((x ? entry(s)),(y ? entry(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) .
eq q12 = ((x @ runnable(s)) |- (x ? entry(s))) .
eq q13 = ((y @ runnable(s)) |- (y ? entry(s))) .
ops i11 i12 : -> Inference .
eq antecedent(i11) = (q11,q12) .
trans ((x @ runnable(s)),(y ? entry(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) => consequent(i11) .
trans consequent(i11) => ((x @ runnable(s)),(y ? entry(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) .
eq antecedent(i12) = (consequent(i11),q13) .
trans ((x @ runnable(s)),(y @ runnable(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) => consequent(i12) .
trans consequent(i12) => ((x @ runnable(s)),(y @ runnable(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = (nil |- (x @ runnable(s))) .
eq q22 = (nil |- (y @ runnable(s))) .
eq antecedent(i2) = (consequent(i12),q21,q22) .
trans (nil |- (x ahead(s) y),(x = y),(y ahead(s) x)) => consequent(i2) .
trans consequent(i2) => (nil |- (x ahead(s) y),(x = y),(y ahead(s) x)) .

ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = ((x block(s) x) |- nil) .
eq q32 = ((x = y),(x block(s) y) |- (x block(s) x)) .
eq antecedent(i3) = (consequent(i2),q31,q32) .
trans ((x block(s) y) |- (x ahead(s) y),(y ahead(s) x)) => consequent(i3) .
trans consequent(i3) => ((x block(s) y) |- (x ahead(s) y),(y ahead(s) x)) .

ops i4 : -> Inference .
ops q41 q42 q43 : -> Sequent .
eq q41 = ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) .
eq q42 = ((x block(s) y) |- (x @ executed(s))) .
eq q43 = ((x prior(s) y) |- (x [prior(s);ahead(s)] y)) .
eq antecedent(i4) = (q41,q42,q43) .
trans ((x block(s) y),(y ahead(s) x) |- (x [prior(s);ahead(s)] y)) => consequent(i4) .
trans consequent(i4) => ((x block(s) y),(y ahead(s) x) |- (x [prior(s);ahead(s)] y)) .

ops i5 : -> Inference .
ops q51 q52 : -> Sequent .
eq q51 = ((x block(s) y),(x ahead(s) y),(y @ executed(s)) |- nil) .
eq q52 = (nil |- (y @ executed(s)),(priority(y)(s) = assign(y))) .
eq antecedent(i5) = (q51,q52) .
trans ((x block(s) y),(x ahead(s) y) |- (priority(y)(s) = assign(y))) => consequent(i5) .
trans consequent(i5) => ((x block(s) y),(x ahead(s) y) |- (priority(y)(s) = assign(y))) .

ops i6 : -> Inference .
ops q61 q62 q63 : -> Sequent .
eq q61 = ((x block(s) y),(assign(y) > priority(x)(s)) |- nil) .
eq q62 = ((priority(y)(s) = assign(y)),(priority(y)(s) > priority(x)(s)) |- (assign(y) > priority(x)(s))) .
eq q63 = ((y prior(s) x) |- (priority(y)(s) > priority(x)(s))) .
eq antecedent(i6) = (q61,q62,q63) .
trans ((x block(s) y),(priority(y)(s) = assign(y)),(y prior(s) x) |- nil) => consequent(i6) .
trans consequent(i6) => ((x block(s) y),(priority(y)(s) = assign(y)),(y prior(s) x) |- nil) .

ops i7 : -> Inference .
eq antecedent(i7) = (consequent(i5),consequent(i6)) .
trans ((x block(s) y),(x ahead(s) y),(y prior(s) x) |- nil) => consequent(i7) .
trans consequent(i7) => ((x block(s) y),(x ahead(s) y),(y prior(s) x) |- nil) .

ops i8 : -> Inference .
ops q81 q82 : -> Sequent .
eq q81 = ((x ahead(s) y),(x [prior(s)] y) |- (x [prior(s);ahead(s)] y)) .
eq q82 = (nil |- (x [prior(s)] y),(y prior(s) x)) .
eq antecedent(i8) = (consequent(i7),q81,q82) .
trans ((x ahead(s) y),(x block(s) y) |- (x [prior(s);ahead(s)] y)) => consequent(i8) .
trans consequent(i8) => ((x ahead(s) y),(x block(s) y) |- (x [prior(s);ahead(s)] y)) .

ops i9 : -> Inference .
eq antecedent(i9) = (consequent(i3),consequent(i4),consequent(i8)) .
eq ((x block(s) y) |- (x [prior(s);ahead(s)] y)) = consequent(i9) .

red claim .
close

#!python
%STATE + LK> red claim .
-- reduce in %STATE + LK : (claim):Prop

** Found [state 2580] (consequent(i9)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1427] (consequent(i8)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 299] (consequent(i7)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2640] (consequent(i6)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 17] (consequent(i5)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 8492] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 597] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 6049] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 243] (consequent(i12)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 235] (consequent(i11)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 138471 rewrites(131.050 sec), 7474263 matches, 77394 memo hits)
Then, we would like to build up a deadlock-free scheduling system to satisfy the hypothesis of the above theorem.

Updated