/*This is a model
of a 2 process real-time scheduler. */
/*Each process is
defined by a triple (period, runtime, deadline*/
/*The goal is to
prove that no deadline is ever missed.
*/
/*When the high
priority wants to run, it must be given the cpu. */
/*The low
priority process will only run if the high priority is idle. */
/* */
/* */
/* */
/* */
/* */
#define maxCycles
5
#define clockMax
20
bit lowDone=0,
highDone=0;
byte clock = 0;
byte
h_state_request = 0;
proctype
high_priority()
{byte numCycles
=0, period=2, runtime=1, deadline= 2, stclock=0;
do
:: (numCycles < maxCycles) ->
numCycles++;
atomic{
clock==h_state_request
->
stclock=clock;
assert(deadline >=clock);
}
deadline = period + deadline;
atomic{clock=clock+runtime;
h_state_request=stclock+period;
}
:: (numCycles >= maxCycles) ->
highDone=1; break
od
}
proctype low_priority()
{byte
l_state_request =0, progress =0, numCycles =0;
byte period =5,runtime=2,deadline=5,stclock=0;
do
:: (numCycles < maxCycles)
->numCycles++;
atomic{(l_state_request >=clock && h_state_request != clock)
->
stclock=clock; progress ++;
}
do
:: (progress < runtime) ->
/* Give high priority a
chance after 1 clock tick*/
atomic{clock++;
(l_state_request <=
clock && h_state_request !=clock) ->
progress++;
}
:: (progress >= runtime)->
progress =0;
atomic{
assert(deadline
>=clock);
deadline = period +
deadline;
l_state_request=stclock + period;
}
break;
od
:: numCycles >= maxCycles ->
lowDone=1; break;
od
}
proctype
clockMonitor()
{end: do
:: timeout->clock++;
:: lowDone && highDone ->
break
od
}
init {
run high_priority();
run low_priority();
run clockMonitor();
}