Standard priorities val P_HIGH = 100; val P_HIGH = 100; val P_NORMAL = 1000; val P_NORMAL = 1000; val P_LOW = 10000; val P_LOW = 10000; Standard declarations UNIT colset UNIT = unit; INT BOOL STRING Analysis declarations clock node STRING value INT next_tick INT colset clock = record node:STRING * value:INT *next_tick:INT; clocks clock colset clocks = list clock; clocks clocks var clocks: clocks; unblk_comp node STRING component STRING port STRING colset unblk_comp = record node:STRING * component:STRING * port: STRING; unblk unblk_comp colset unblk = list unblk_comp; step_ kind STRING port STRING unblk unblk exec_time INT duration INT colset step_ = record kind:STRING * port:STRING * unblk:unblk * exec_time:INT * duration:INT; steps step_ colset steps = list step_; priority 0 99 colset priority = int with 0..99; operation node STRING component STRING operation STRING priority priority deadline INT enqueue_time INT steps steps colset operation = record node:STRING * component:STRING * operation:STRING * priority:priority * deadline:INT * enqueue_time:INT * steps:steps; queue operation colset queue = list operation; timer node STRING period INT offset INT operation operation colset timer = record node:STRING * period:INT * offset: INT * operation:operation; timers timer colset timers = list timer; timers timers var timers:timers; scheme FIFO PFIFO EDF colset scheme = with FIFO | PFIFO | EDF; cmq component STRING scheme scheme queue queue colset cmq = record component:STRING * scheme:scheme * queue:queue; cmql cmq colset cmql = list cmq; ncmq node STRING cmql cmql colset ncmq = record node:STRING * cmql:cmql; ncmql ncmq colset ncmql = list ncmq; ncmql ncmql var ncmql:ncmql; component_thread node STRING component STRING priority INT operation queue colset component_thread = record node:STRING * component:STRING * priority:INT * operation:queue; component_threads component_thread colset component_threads = list component_thread; node_threads node STRING threads component_threads colset node_threads = record node:STRING * threads:component_threads; node_thread_list node_threads colset node_thread_list = list node_threads; node_thread_list nths var nths:node_thread_list; component_thread th var th:component_thread; component_threads bths rths var bths, rths:component_threads; interaction node STRING enqueue_time INT operation operation colset interaction = record node:STRING * enqueue_time:INT * operation:operation; waiting_interactions interaction colset waiting_interactions = list interaction; waiting_interactions wi var wi:waiting_interactions; induced_operation node STRING port STRING operation operation colset induced_operation = record node: STRING * port:STRING * operation:operation; interactions induced_operation colset interactions = list induced_operation; interactions interactions var interactions:interactions; completed_operation node STRING component STRING operation STRING enqueue_time INT completion_time INT deadline INT colset completed_operation = record node:STRING * component:STRING * operation:STRING * enqueue_time:INT * completion_time:INT * deadline:INT; completed_operations completed_operation colset completed_operations = list completed_operation; completed_operations copns var copns:completed_operations; unblocked_thread node STRING unblock_time INT thread component_thread colset unblocked_thread = record node:STRING * unblock_time:INT * thread:component_thread; waiting_threads unblocked_thread colset waiting_threads = list unblocked_thread; waiting_threads wths var wths:waiting_threads; Functions "functions/generic.sml" use "functions/generic.sml"; "functions/clock.sml" use "functions/clock.sml"; "functions/timers.sml" use "functions/timers.sml"; "functions/cmq.sml" use "functions/cmq.sml"; "functions/threading.sml" use "functions/threading.sml"; Timers timers <%- timer_tokens %> Clocks clocks <%- clock_tokens %> CMQ ncmql <%- message_queue_tokens %> Components node_thread_list <%- component_thread_tokens %> Running Threads component_threads 1`[] Waiting to Enqueue waiting_interactions 1`[] Component Interactions interactions <%- interaction_tokens %> Completed_Operations completed_operations 1`[] Blocked Threads component_threads 1`[] Waiting to Unblock waiting_threads 1`[] COMPETING THREADS component_thread Timer_Expiry [ExpiryGuard clocks timers] Schedule_Thread [ScheduleGuard clocks ncmql nths rths] Execute_Thread [ExecuteGuard clocks timers rths wi wths] Enqueue_Operation [EnqueueGuard clocks wi] Preempt_Thread [PreemptGuard clocks rths] Advance_Time [AdvanceTimeGuard clocks] P_LOW Unblock_Thread [UnblockGuard clocks wths] ESTABLISH ORDER P_HIGH timers (UpdateTimers clocks timers) ncmql (EnqueueAllOperations (ListTimerOperations clocks timers) ncmql) nths (RemoveThreads clocks ncmql nths) ncmql (ScheduleThreads clocks ncmql nths rths) rths (DequeueOperations clocks ncmql nths rths) clocks clocks rths (ExecuteThreads clocks timers wi wths rths) clocks (UpdateClocks clocks timers wi rths) wi (InduceOperations wi rths interactions clocks) wi (EnqueueAllOperations (GetOperationsList clocks wi) ncmql) ncmql clocks rths (UpdateRunningThreads clocks rths) (EstablishOrder clocks rths nths) nths timers clocks (UpdateClocksOnPreemption clocks rths) (RemoveOperations clocks wi) interactions clocks timers wi (AdvanceTime (GetAdvanceTime clocks timers wi wths ncmql nths rths) clocks timers wi wths) copns (SaveAllCompletedOperations copns clocks timers wi wths rths) bths (GetAllBlockedThreads (RemoveBlockedThreads (UnblockThreads wths rths bths clocks timers wi) bths) clocks timers wi wths rths) wths (UnblockThreads wths rths bths clocks timers wi) wths (RemoveUnblockedThreads (GetThreadsToRemoveFromWTHS clocks wths) wths) nths (EstablishOrderUponUnblock clocks (GetUnblockableThreads clocks wths) nths) wths ncmql nths rths clocks copns (SaveUnblockedCompletedOperations copns wths) th nths (Initialize th nths)