module PROCESSOR (TYPES, SIZE, VIRTUAL) is

-------------------------------------------------------------------------------

process PROCESSOR [ST, LD_RQ, LD_RSP, WAKEUP, BOOT, MSG: any]
                  (id:Pid, ext:Extension) is
   var j: Job_Desc, s: Job_Desc_Stack in
      s := empty_stack;
      BOOT (id, ext);
      loop
         WAKEUP (id);
         loop main_loop in
            LD_RQ (id);
            LD_RSP (id, ?j);
            case j in
              EXEC (any PC, any Int) ->
                  EXECUTE [ST, MSG] (id, j, s?)
            | WAIT_SLAVE -> null
            | DONE ->
                  -- all slaves terminated, pop the continuation
                  if (is_empty (s)) then
                     break main_loop
                  else
                     j := head (s);
                     s := pop (s);
                     EXECUTE [ST, MSG] (id, j, s?)
                  end if
            | NONE -> break main_loop
            end case
         end loop
      end loop
   end var
end process

-------------------------------------------------------------------------------

end module