pcp_scheduler {Semaphore : TYPE; NumberOfTasks : NATURAL, task_descriptors : pcp_task{Semaphore; NumberOfTasks}!TaskDescriptors } : CONTEXT = BEGIN taskCtx : CONTEXT = pcp_task{Semaphore; NumberOfTasks}; rsrcCtx : CONTEXT = pcp_rsrc{Semaphore; NumberOfTasks, task_descriptors}; jobSetCtx : CONTEXT = set{taskCtx!JobIdx;}; semSetCtx : CONTEXT = set{Semaphore;}; JobIdx : TYPE = taskCtx!JobIdx; RSRC : TYPE = rsrcCtx!RSRC; period(j : JobIdx) : NATURAL = taskCtx!period(j, task_descriptors); budget(j : JobIdx) : NATURAL = taskCtx!budget(j, task_descriptors); lcm(m : NATURAL, n : NATURAL) : NATURAL = math!lcm(m,n); % maximum period should be the lcm of the period of each task. compute_max_period(result : NATURAL, i : NATURAL) : NATURAL = IF i <= NumberOfTasks THEN compute_max_period(lcm(result, period(i)), i+1) ELSE result ENDIF; max_period : NATURAL = IF NumberOfTasks = 0 THEN 1 ELSIF NumberOfTasks = 1 THEN period(1) ELSE compute_max_period(period(1), 2) ENDIF; compute_max_budget(result : NATURAL, i : NATURAL) : NATURAL = IF i <= NumberOfTasks THEN compute_max_budget(max(result, budget(i)), i+1) ELSE result ENDIF; max_budget : NATURAL = IF NumberOfTasks = 0 THEN 0 ELSIF NumberOfTasks = 1 THEN budget(1) ELSE compute_max_budget(budget(1), 2) ENDIF; ClockRange : TYPE = [0..(max_period - 1)]; PC : TYPE = [0..max_budget]; % PC = 0 means the process is sleeping adjust(val : NATURAL) : ClockRange = IF val < max_period THEN val ELSE val - max_period ENDIF; priority(j : JobIdx) : NATURAL = rsrcCtx!priority(j); uses_sem?(j : JobIdx, s : Semaphore) : BOOLEAN = rsrcCtx!uses_sem?(j, s); ceiling(s : Semaphore) : NATURAL = rsrcCtx!ceiling(s); blocked?(r : RSRC, j : JobIdx) : BOOLEAN = rsrcCtx!blocked?(r, j); blk(r : RSRC, j : JobIdx) : jobSetCtx!Set = rsrcCtx!blk(r, j); % In the absence of blocking, jobs of high priority are executed first precedes?(j : JobIdx, k : JobIdx) : BOOLEAN = priority(j) >= priority(k); JobState : TYPE = ARRAY JobIdx OF PC; sleeping?(j : JobIdx, job_state : JobState) : BOOLEAN = job_state[j] = 0; end_of_budget?(j : JobIdx, job_state : JobState) : BOOLEAN = job_state[j] = budget(j); ready_to_execute?(j : JobIdx, job_state : JobState) : BOOLEAN = NOT sleeping?(j, job_state); topjob?(j : JobIdx, rsrc : RSRC, job_state : JobState) : BOOLEAN = ready_to_execute?(j, job_state) AND (FORALL (k : JobIdx): ready_to_execute?(k, job_state) => precedes?(j, k)); eligible?(j : JobIdx, rsrc : RSRC, job_state : JobState) : BOOLEAN = (topjob?(j, rsrc, job_state) AND NOT blocked?(rsrc, j)) OR (EXISTS (k : JobIdx): topjob?(k, rsrc, job_state) AND blocked?(rsrc, k) AND jobSetCtx!contains?(blk(rsrc, k), j)); lock(r : RSRC, j : JobIdx, s : Semaphore) : RSRC = rsrcCtx!alloc_step(rsrcCtx!wakeup(r, j), j, s); unlock(r : RSRC, j : JobIdx, s : Semaphore) : RSRC = rsrcCtx!release_step(rsrcCtx!wakeup(r, j), j, s); unlock_all(r : RSRC, j : JobIdx) : RSRC = rsrcCtx!release_all_step(r, j); step(r : RSRC, j : JobIdx) : RSRC = rsrcCtx!wakeup(r, j); Turn : TYPE = DATATYPE job_turn(job_turn_id : JobIdx), idle_turn END; Command : TYPE = DATATYPE cmd_lock(cmd_lock_s : Semaphore), cmd_unlock(cmd_unlock_s : Semaphore), cmd_unlock_all, cmd_step END; valid_command?(j : JobIdx, c : Command) : BOOLEAN = (IF cmd_lock?(c) THEN uses_sem?(j, cmd_lock_s(c)) ELSIF cmd_unlock?(c) THEN uses_sem?(j, cmd_unlock_s(c)) ELSE TRUE ENDIF); turn?(t : Turn, j : JobIdx) : BOOLEAN = job_turn?(t) AND job_turn_id(t) = j; scheduler : MODULE = BEGIN LOCAL clock : ClockRange LOCAL dispatch : ARRAY JobIdx OF ClockRange LOCAL job_state : JobState OUTPUT turn : Turn LOCAL rsrc : RSRC INPUT cmd : Command INITIALIZATION clock = 0; dispatch = [ [j : JobIdx] 0]; job_state = [ [j : JobIdx] 0]; rsrc = rsrcCtx!initial_rsrc; turn = idle_turn TRANSITION clock' = adjust(clock + 1); job_state' = [ [j : JobIdx] IF sleeping?(j, job_state) AND dispatch[j] = clock THEN 1 ELSIF turn?(turn, j) THEN IF end_of_budget?(j, job_state) THEN 0 % go to sleep ELSE job_state[j] + 1 ENDIF % increase the program counter ELSE job_state[j] ENDIF ]; dispatch' = [ [j : JobIdx] IF dispatch[j] = clock THEN adjust(dispatch[j] + period(j)) ELSE dispatch[j] ENDIF]; rsrc' = (IF turn = idle_turn THEN rsrc ELSE LET j : JobIdx = job_turn_id(turn) IN IF end_of_budget?(j, job_state) THEN unlock_all(rsrc, j) % ignore the cmd... ELSIF cmd_lock?(cmd) AND uses_sem?(j, cmd_lock_s(cmd)) THEN lock(rsrc, j, cmd_lock_s(cmd)) ELSIF cmd_unlock?(cmd) AND uses_sem?(j, cmd_unlock_s(cmd)) THEN unlock(rsrc, j, cmd_unlock_s(cmd)) ELSIF cmd_unlock_all?(cmd) THEN unlock_all(rsrc, j) ELSE rsrc ENDIF ENDIF); [ ([] (j : JobIdx ) : eligible?(j, rsrc, job_state') --> turn' = job_turn(j)) [] ELSE --> turn' = idle_turn ] END; deadline_missed? (dispatch : ARRAY JobIdx OF ClockRange, job_state : JobState, clock : ClockRange) : BOOLEAN = (EXISTS (j : JobIdx) : dispatch[j] = clock AND NOT sleeping?(j, job_state)); deadlock? (job_state : JobState, t : Turn) : BOOLEAN = idle_turn?(t) AND (EXISTS (j : JobIdx) : ready_to_execute?(j, job_state)); consistent1? (job_state : JobState) : BOOLEAN = (FORALL (j : JobIdx) : job_state[j] <= budget(j)); END