-- File: [Indigo]<Sakura>Dragon>DragonCacheImpl.sak
-- Dragon Cache
-- 23-Mar-82 13:02:29

DIRECTORY
  ConvertUnsafe: TYPE, 
  DragonCache: TYPE, 
  Inline: TYPE, 
  SakuraRT: TYPE, 
  SimIO: TYPE;

DragonCacheImpl1: MONITOR
  IMPORTS ConvertUnsafe, Inline, SakuraRT, SimIO
  EXPORTS DragonCache
  
  -- The functionality of Dragon cache chip is described under the following 
  --conventions: there are two main processes, a process to watch the processor bus
  --commands (PbusFetch), and a process to watch the memory bus commands
  --(BackDoor, backdoor operations).  Furthermore, PbusFetch cooperates with 
  --several other processes to allow overlapping of pipline operations: MProc is a 
  --process that is invoked from PbusFetch and invokes Mbus operations directly.  
  --Operations associated with Pbus commands are all split into two parts so that 
  --they can be piplined.  All the front parts of these operations are inside 
  --PbusFetch, so they do not constitute independent processes.  The latter parts 
  --are all independent processes.  They are FetchTransport, StoreTransport, and 
  --DoMapOpTransport.  
  
  -- Communications among processes:
  --Communication between PbusFetch and MProc is done through two global
  --variables: DoMProc and MProcDone.  The communication between PbusFetch
  --and transport processes, FetchTransport, StoreTransport, and
  --DoMapOpTransport, is done by global variables, FetchTransportGo, 
  --StoreTransportGo, and DoMapOpTransportGo, and ~Reject for the other
  --direction.
  
  = BEGIN
  Cell: TYPE = RECORD [vp: LONG CARDINAL, 
                       rp: LONG CARDINAL, 
                       bl: INTEGER [0..37B], 
                       D: ARRAY INTEGER [0..3] OF LONG CARDINAL, 
                       VpValid, RpValid, RpDirty, CEDirty, Shared, TIP: BOOLEAN]; 
  MProcType: TYPE = PROC; 
  

  -- Constants
  DataArraySize: CARDINAL = 64; 
  ProcessorNum: STRING = "Proc2: "; 
  
  -- Global variables
  FetchTransportGo, StoreTransportGo, DoMapOpTransportGo, Holding, DoMProc, MProcDone, 
  PRq, NewRq, MRq, Orph, MCMD: BOOLEAN; 
  Instruction: DragonCache.PbusOp; 
  DataIndex, VictimIndex: CARDINAL; 
  RqBL, PBL, MBL: INTEGER [0..37B]; 
  PWord, MWord: INTEGER [0..3]; 
  RqVP, MVP, RqData, PResult, PRP, MRP, MOResult, MRdData, MWData: LONG CARDINAL; 
  Data: ARRAY INTEGER [0..DataArraySize) OF Cell; 
  MOp: MProcType; 
  MInst: DragonCache.MbusCommand; 
  MapOp: DragonCache.MapOpKind; 
  RpDirtyReg: BOOLEAN; -- This register is set by ReadMap or PartialMatch
  
  PageFault: SIGNAL = CODE; 
  WriteViolation: SIGNAL = CODE; 
  
  CheckVal: PUBLIC ENTRY PROC
       [vp: LONG CARDINAL, bl: INTEGER [0..37B], word: INTEGER [0..3], val: LONG 
          CARDINAL] = {
    loc: CARDINAL; 
    matched: BOOLEAN;
    [matched, loc] ← FullVpMatch[vp, bl]; 
    IF NOT matched THEN ERROR; 
    IF Data[loc].D[word] # val THEN ERROR}; 
  
  Cache: PUBLIC PROC
       [Op: SakuraRT.Handle, PDataIn: SakuraRT.Handle, MDataIn: SakuraRT.Handle, 
        ClockA, ClockB, CMDIn, RQ, SharedIn, Grant: SakuraRT.Handle, 
        Exception, Reject, SharedOut, CMDOut, Rq: SakuraRT.Handle, 
        PDataOut: SakuraRT.Handle, MDataOut: SakuraRT.Handle] = {
    
    -- PbusFetch process procedures
    
    PbusFetch: PROC = {
      success: BOOLEAN;
      {ENABLE {ABORTED => GO TO Aborted};
       DO SakuraRT.GetNew[ClockA, TRUE]; NULL; --A (Phase A)
          IF NARROW[SakuraRT.Get[RQ], REF BOOLEAN]↑ AND 
               NOT NARROW[SakuraRT.Get[Reject], REF BOOLEAN]↑ THEN 
             {SakuraRT.Put[Exception, NEW[BOOLEAN ← FALSE]]; 
              WITH b: NARROW[SakuraRT.Get[PDataIn], REF DragonCache.PbusType]↑ SELECT FROM 
                Instruction => {RqVP ← b.vp; RqBL ← b.bl; PWord ← b.word}
                ENDCASE => ERROR; 
              Instruction ← NARROW[SakuraRT.Get[Op], REF DragonCache.PbusOp]↑; 
              SakuraRT.GetNew[ClockB, TRUE];
               [success, DataIndex] ← FullVpMatch[RqVP, RqBL]; --M (Phase B)
              {ENABLE {
                 PageFault => 
                   {SakuraRT.Put[PDataOut, NEW[DragonCache.PbusType ← [Data[-1]]]]; 
                    SakuraRT.Put[Exception, NEW[BOOLEAN ← TRUE]]};
                 WriteViolation => 
                   {SakuraRT.Put[PDataOut, NEW[DragonCache.PbusType ← [Data[0]]]]; 
                    SakuraRT.Put[Exception, NEW[BOOLEAN ← TRUE]]}};
               SELECT Instruction FROM 
                 Fetch => CallFetch[success];
                 FetchHold => 
                   CallFetchHold
                     [success
                      ! PageFault => 
                          {SakuraRT.Put[PDataOut, NEW[DragonCache.PbusType ← [Data[-
                                                                                   1]]]]; 
                           Holding ← FALSE; SakuraRT.Put[Exception, NEW[BOOLEAN ← TRUE]]};
                        WriteViolation => 
                          {SakuraRT.Put[PDataOut, NEW[DragonCache.PbusType ← [Data[0]]]]; 
                           SakuraRT.Put[Exception, NEW[BOOLEAN ← TRUE]]}];
                 Store => CallStore[success];
                 MapOp => CallMapOp[success]
                 ENDCASE}}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; 
    
    WaitForTIP: PROC = {
      SakuraRT.Put[Reject, NEW[BOOLEAN ← TRUE]]; 
      DO SakuraRT.Delay[30]; 
         IF Data[DataIndex].TIP 
            THEN {SakuraRT.GetNew[ClockB, TRUE]; NULL; 
                  LOOP} 
            ELSE EXIT
         ENDLOOP}; 
    
    CallFetch: PROC [success: BOOLEAN] = {
      -- Started at Phase B
      index: CARDINAL;
      IF success --hit
         THEN {WaitForTIP[]; 
               SakuraRT.Put[Reject, NEW[BOOLEAN ← FALSE]]; 
               FetchTransportGo ← TRUE; 
               Holding ← FALSE} 
         ELSE {SakuraRT.Put[Reject, NEW[BOOLEAN ← TRUE]]; 
               Holding ← FALSE; 
               SakuraRT.GetNew[ClockA, TRUE]; Holding ← TRUE; --R (Phase A)
               SakuraRT.Delay[10]; 
               PRq ← TRUE; --T (Phase B)
               WaitForGrant[]; 
               WriteBackVictimIfDirty[]; 
               [success, index] ← PartialMatch[RqVP]; 
               PRP ← Data[index].rp; 
               SakuraRT.GetNew[ClockB, TRUE];
                IF NOT success THEN CallMProc[ReadMap, "ReadMap"]; 
               IF success THEN CallMProc[ReadQuadMatch, "ReadQuad"] 
                  ELSE CallMProc[ReadQuad, "ReadQuad"]; 
               PRq ← FALSE; 
               SakuraRT.Put[Reject, NEW[BOOLEAN ← FALSE]]; 
               [success, DataIndex] ← FullVpMatch[RqVP, RqBL]; 
               IF NOT success THEN ERROR; -- This is a description error
               FetchTransportGo ← TRUE}}; 
    
    CallFetchHold: PROC [success: BOOLEAN] = {
      -- Started at Phase B
      IF NOT Holding THEN 
         {SakuraRT.Put[Reject, NEW[BOOLEAN ← TRUE]]; 
          SakuraRT.GetNew[ClockA, TRUE]; NULL; 
          SakuraRT.Delay[10]; 
          PRq ← TRUE; 
          WaitForGrant[]; 
          SakuraRT.GetNew[ClockB, TRUE]; Holding ← TRUE}; 
      CallFetch[success]}; 
    
    CallStore: PROC [success: BOOLEAN] = {
      SakuraRT.Put[Reject, NEW[BOOLEAN ← TRUE]]; 
      SakuraRT.GetNew[ClockA, TRUE];
       WITH b: NARROW[SakuraRT.Get[PDataIn], REF DragonCache.PbusType]↑ SELECT FROM 
        Data => RqData ← b.data
        ENDCASE => ERROR; 
      WaitForTIP[]; 
      IF NOT success THEN 
         {SakuraRT.Delay[10]; 
          PRq ← TRUE; 
          WaitForGrant[]; 
          WriteBackVictimIfDirty[]; 
          SakuraRT.GetNew[ClockB, TRUE];
           {[success, DataIndex] ← PartialMatch[RqVP]; 
            PRP ← Data[DataIndex].rp; 
            IF NOT success THEN CallMProc[ReadMapAndSetRpDirty, "ReadMapAndSetRpDirty"]}; 
          SakuraRT.GetNew[ClockB, TRUE];
           IF success THEN CallMProc[ReadQuadMatch, "ReadQuad"] 
              ELSE CallMProc[ReadQuad, "ReadQuad"]}; 
      SakuraRT.GetNew[ClockB, TRUE]; [success, DataIndex] ← FullVpMatch[RqVP, RqBL]; 
      Data[DataIndex].CEDirty ← TRUE; 
      IF NOT Data[DataIndex].RpDirty THEN 
         {IF NOT PRq THEN {PRq ← TRUE; WaitForGrant[]}; 
          CallMProc[ReadMapAndSetRpDirty, "ReadMapAndSetRpDirty"]}; 
      IF NOT Data[DataIndex].Shared THEN StoreTransportGo ← TRUE 
         ELSE {Data[DataIndex].D[PWord] ← RqData; 
               IF NOT PRq THEN {PRq ← TRUE; WaitForGrant[]}; 
               CallMProc[WriteSingle, "WriteSingle"]}; 
      SakuraRT.Put[Reject, NEW[BOOLEAN ← FALSE]]; 
      PRq ← FALSE}; -- CallStore
    
    CallMapOp: PROC [success: BOOLEAN] = {
      -- Started at Phase B
      SakuraRT.Put[Reject, NEW[BOOLEAN ← TRUE]]; 
      SakuraRT.GetNew[ClockA, TRUE]; NULL; 
      SakuraRT.Delay[10]; 
      PRq ← TRUE; 
      WaitForGrant[]; 
      SakuraRT.GetNew[ClockA, TRUE];
       WITH b: NARROW[SakuraRT.Get[PDataIn], REF DragonCache.PbusType]↑ SELECT FROM 
        Data => RqData ← b.data
        ENDCASE => ERROR; 
      CallMProc[DoMapOp, "DoMapOp"]; 
      PRq ← FALSE}; -- CallMapOp
    
    CallMProc: PROC [procedure: MProcType, name: REF TEXT] = {
      -- Starts in Phase B and finishes in Phase B
      st: LONG STRING ← [25];
      ConvertUnsafe.AppendRefText[st, name]; 
      WaitMProcReallyDone[]; 
      SetMProcDone[FALSE]; 
      SetDoMProc[TRUE]; 
      MOp ← procedure; 
      SimIO.WF2["     %sMbus op: %s started*n", ProcessorNum, st]; 
      DO SakuraRT.GetNew[ClockB, TRUE]; IF IsMProcDone[] THEN EXIT
         ENDLOOP; 
      SimIO.WF2["     %sMbus op: %s finished*n", ProcessorNum, st]}; 
    -- CallMProc
    
    WaitMProcReallyDone: PROC = {
      -- Starts in Phase B
      DO SakuraRT.Delay[30]; 
         IF IsMProcReallyDone[] THEN EXIT; 
         SakuraRT.GetNew[ClockB, TRUE]; NULL
         ENDLOOP}; 
    
    SetMProcReallyDone: ENTRY PROC [val: BOOLEAN] = {
      MProcReallyDone ← val}; 
    
    IsMProcReallyDone: ENTRY PROC RETURNS [BOOLEAN] = {
      RETURN [MProcReallyDone]}; 
    
    MProcReallyDone: BOOLEAN ← TRUE; 
    
    WriteBackVictimIfDirty: PROC = {
      -- Starts at Phase A
      MRP ← Data[VictimIndex].rp; 
      MBL ← Data[VictimIndex].bl; 
      IF Data[VictimIndex].RpValid AND Data[VictimIndex].CEDirty THEN 
         {CallMProc[WriteQuad, "WriteQuad"]; 
          Data[VictimIndex].CEDirty ← FALSE}}; -- WriteBackVictimIfNotClean
    
    WaitForGrant: PROC = {
      DO SakuraRT.GetNew[ClockA, TRUE]; IF NARROW[SakuraRT.Get[Grant], REF BOOLEAN]↑ THEN 
                                           EXIT
         ENDLOOP}; -- WaitForGrant
    


    -- FetchTransport process procedures
    
    FetchTransport: PROC = {
      -- Starts at Phase B
      {ENABLE {ABORTED => GO TO Aborted};
       DO SakuraRT.GetNew[ClockA, TRUE]; NULL; --R (Phase A)
          IF FetchTransportGo THEN 
             {PResult ← Data[DataIndex].D[PWord]; 
              FetchTransportGo ← FALSE; 
              SakuraRT.GetNew[ClockB, TRUE];
               SakuraRT.Put[PDataOut, NEW[DragonCache.PbusType ← [Data[PResult]]]]}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; 
    
    StoreTransport: PROC = {
      -- Starts at Phase B
      index, pword: CARDINAL; 
      success: BOOLEAN;
      {ENABLE {ABORTED => GO TO Aborted};
       DO SakuraRT.GetNew[ClockB, TRUE]; {pword ← PWord; 
                                          [success, index] ← FullVpMatch[RqVP, RqBL]}; 
          SakuraRT.GetNew[ClockA, TRUE]; IF StoreTransportGo THEN 
                                            {IF NOT success THEN ERROR; 
                                             Data[index].D[pword] ← RqData; 
                                             StoreTransportGo ← FALSE}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; -- StoreTransport
    
    DoMapOpTransport: PROC = {
      {ENABLE {ABORTED => GO TO Aborted};
       DO SakuraRT.GetNew[ClockB, TRUE]; NULL; --  (B)
          IF DoMapOpTransportGo THEN 
             {NewRq ← TRUE; 
              MOResult ← MRdData; 
              SakuraRT.Put[Reject, NEW[BOOLEAN ← FALSE]]; 
              SakuraRT.GetNew[ClockA, TRUE]; {PResult ← MOResult; 
                                              NewRq ← FALSE}; 
              SakuraRT.GetNew[ClockB, TRUE];
               {IF Inline.BITAND[Inline.HighHalf[PResult], 40000B] # 0 THEN 
                   SakuraRT.Put[Exception, NEW[BOOLEAN ← TRUE]]; 
                SakuraRT.Put[PDataOut, NEW[DragonCache.PbusType ← [Data[PResult]]]]}}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; -- DoMapOpTransport
    


    -- MProc process procedures
    
    MProc: PROC = {
      {ENABLE {ABORTED => GO TO Aborted};
       SetMProcDone[FALSE]; 
       DO SakuraRT.GetNew[ClockA, TRUE]; NULL; 
          IF IsDoMProc[] THEN 
             {SetDoMProc[FALSE]; 
              SakuraRT.Put[CMDOut, NEW[BOOLEAN ← TRUE]]; 
              MOp[]}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; 
    
    SetDoMProc: ENTRY PROC [val: BOOLEAN] = {
      DoMProc ← val}; 
    
    IsDoMProc: ENTRY PROC RETURNS [BOOLEAN] = {
      RETURN [DoMProc]}; 
    
    SetMProcDone: ENTRY PROC [val: BOOLEAN] = {
      MProcDone ← val}; 
    
    IsMProcDone: ENTRY PROC RETURNS [BOOLEAN] = {
      RETURN [MProcDone]}; 
    
    WriteQuad: PROC = {
      i: CARDINAL; 
      WriteOneWord: PROC [pword: INTEGER [0..3]] = {
        SakuraRT.GetNew[ClockB, TRUE]; MWData ← Data[VictimIndex].D[pword]; 
        SakuraRT.GetNew[ClockA, TRUE];
         SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Data[MWData]]]]};
      -- WriteOneWord
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Instruction[WriteQuad, 
                                                                     MRP, MBL, 0]]]]; 
      SakuraRT.GetNew[ClockB, TRUE]; MWData ← Data[VictimIndex].D[0]; 
      SakuraRT.Delay[20]; 
      SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
      SakuraRT.GetNew[ClockA, TRUE];
       SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Data[MWData]]]]; 
      FOR i IN [1..3] DO
          WriteOneWord[i]
          ENDLOOP; 
      SakuraRT.GetNew[ClockB, TRUE]; SetMProcDone[TRUE]; 
      SetMProcReallyDone[TRUE]}; -- WriteQuad
    
    ReadMap: PROC = {
      fault: BOOLEAN;
      MVP ← RqVP; 
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [MapCommand[ReadMap, 
                                                                    , , , MVP]]]]; 
      SakuraRT.GetNew[ClockB, TRUE]; SakuraRT.Delay[20]; 
      SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
      fault ← WaitMapOpDone[]; 
      IF fault THEN SIGNAL PageFault; 
      WITH b: NARROW[SakuraRT.Get[MDataIn], REF DragonCache.MbusType]↑ SELECT FROM 
        MapCommand => {MRP ← b.vp; RpDirtyReg ← b.rpdirty}
        ENDCASE => ERROR; 
      SetMProcDone[TRUE]; 
      SetMProcReallyDone[TRUE]}; 
    
    ReadMapAndSetRpDirty: PROC = {
      fault: BOOLEAN;
      MVP ← RqVP; 
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [MapCommand[ReadMapAndSetRpDirty, 
                                                                    , , , MVP]]]]; 
      SakuraRT.GetNew[ClockB, TRUE]; SakuraRT.Delay[20]; 
      SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
      fault ← WaitMapOpDone[]; 
      IF fault THEN SIGNAL PageFault; 
      WITH b: NARROW[SakuraRT.Get[MDataIn], REF DragonCache.MbusType]↑ SELECT FROM 
        MapCommand => {MRP ← b.vp; RpDirtyReg ← b.rpdirty}
        ENDCASE => ERROR; 
      SetMProcDone[TRUE]; 
      SetMProcReallyDone[TRUE]}; 
    
    ReadQuadMatch: PROC = {
      MRP ← PRP; 
      ReadQuad[]}; 
    
    ReadQuad: PROC = {
      ReadOneWord: PROC = {
        IF NOT Orph THEN ReadDataFromBus[@Data[index].D[pword]]}; 
      success: BOOLEAN; 
      pword: CARDINAL ← PWord; 
      index: CARDINAL;
      PBL ← RqBL; 
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Instruction[ReadQuad, 
                                                                     MRP, PBL, pword]]]]; 
      WITH b: NARROW[SakuraRT.Get[MDataIn], REF DragonCache.MbusType]↑ SELECT FROM 
        Instruction => {MRP ← b.rp; MBL ← b.bl; MWord ← b.word}
        ENDCASE => ERROR; 
      SakuraRT.GetNew[ClockB, TRUE]; MRq ← TRUE; -- (Phase B, t2)
      SakuraRT.Delay[20]; 
      SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
      SakuraRT.GetNew[ClockA, TRUE]; [success, index] ← FullRpMatch[MRP, MBL]; 
      -- (Phase A, t3)
      SakuraRT.GetNew[ClockB, TRUE]; -- (Phase B, t4)
      {Orph ← success; 
       IF NOT success THEN index ← VictimIndex}; 
      SakuraRT.GetNew[ClockA, TRUE]; IF NOT success THEN -- (Phase A, t5)
                                        {Data[index].rp ← MRP; 
                                         Data[index].bl ← MBL; 
                                         Data[index].RpValid ← TRUE; 
                                         Data[index].Shared ← FALSE; 
                                         Data[index].CEDirty ← FALSE; 
                                         Data[index].RpDirty ← RpDirtyReg}; 
      SakuraRT.GetNew[ClockB, TRUE]; -- (Phase B, t6) -- Data[index].vp ← RqVP; 
      Data[index].VpValid ← TRUE; 
      Data[index].Shared ← NARROW[SakuraRT.Get[SharedIn], REF BOOLEAN]↑; 
      VictimIndex ← (VictimIndex + 1) MOD DataArraySize; 
      SakuraRT.GetNew[ClockA, TRUE]; MCMD ← NARROW[SakuraRT.Get[CMDIn], REF BOOLEAN]↑; 
      -- (Phase A, t7)
      IF MCMD AND MInst = NotReady THEN WaitOneCycle[]; 
      SetMProcDone[TRUE]; 
      SakuraRT.GetNew[ClockB, TRUE]; ReadOneWord[]; -- (Phase B, t8)
      SakuraRT.GetNew[ClockA, TRUE]; pword ← (pword + 1) MOD 4; 
      -- (Phase A, t9)
      SakuraRT.GetNew[ClockB, TRUE];
       -- (Phase B, t10) -- {Data[index].TIP ← TRUE; 
                             ReadOneWord[]; 
                             MRq ← FALSE; 
                             IF NOT Holding THEN NewRq ← TRUE}; 
      SakuraRT.GetNew[ClockA, TRUE]; pword ← (pword + 1) MOD 4; 
      -- (Phase A, t11)
      SakuraRT.GetNew[ClockB, TRUE]; -- (Phase B, t12) 
      {ReadOneWord[]; 
       IF NOT Holding THEN NewRq ← FALSE}; 
      SakuraRT.GetNew[ClockA, TRUE]; pword ← (pword + 1) MOD 4; 
      -- (Phase A, t13)
      SakuraRT.GetNew[ClockB, TRUE]; -- (Phase B, t14) -- {ReadOneWord[]; 
                                                           Data[index].TIP ← FALSE; 
                                                           SetMProcReallyDone[TRUE]}}; 
    
    SetRpDirty: PROC = {
      -- Starts in A
      fault: BOOLEAN;
      PBL ← RqBL; 
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Instruction[SetRpDirty, 
                                                                     MRP, PBL, PWord]]]]; 
      WITH b: NARROW[SakuraRT.Get[MDataIn], REF DragonCache.MbusType]↑ SELECT FROM 
        Instruction => 
          {MRP ← b.rp; 
           MBL ← b.bl; 
           MWord ← b.word}
        ENDCASE => ERROR; 
      SakuraRT.GetNew[ClockB, TRUE]; fault ← WaitMapOpDone[]; 
      IF fault THEN SIGNAL WriteViolation; 
      SetMProcDone[TRUE]; 
      SetMProcReallyDone[TRUE]}; 
    
    WriteSingle: PROC = {
      PBL ← RqBL; 
      PRP ← RqVP; 
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Instruction[WriteSingle, 
                                                                     PRP, PBL, PWord]]]]; 
      NewRq ← TRUE; 
      SakuraRT.GetNew[ClockB, TRUE]; MWData ← RqData; 
      SakuraRT.Delay[20]; 
      SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
      SakuraRT.GetNew[ClockA, TRUE];
       SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Data[MWData]]]]; 
      SakuraRT.GetNew[ClockB, TRUE]; SetMProcDone[TRUE]; 
      NewRq ← FALSE; 
      SetMProcReallyDone[TRUE]}; 
    
    DoMapOp: PROC = {
      fault: BOOLEAN;
      MVP ← RqVP; 
      SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [MapCommand[DoMapOp, 
                                                                    MapOp, 
                                                                    , , MVP]]]]; 
      MCMD ← TRUE; 
      SakuraRT.GetNew[ClockB, TRUE]; MWData ← RqData; 
      SakuraRT.Delay[20]; 
      SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
      SakuraRT.GetNew[ClockA, TRUE];
       SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Data[MWData]]]]; 
      fault ← WaitMapOpDone[]; 
      IF fault THEN SIGNAL PageFault; 
      SetMProcDone[TRUE]; 
      ReadDataFromBus[@MRdData]; 
      DoMapOpTransportGo ← TRUE; 
      SetMProcReallyDone[TRUE]}; -- DoMapOp
    
    WaitMapOpDone: PROC RETURNS [fault: BOOLEAN] = {
      DO SakuraRT.GetNew[ClockB, TRUE]; SakuraRT.Delay[30]; 
         MCMD ← NARROW[SakuraRT.Get[CMDIn], REF BOOLEAN]↑; 
         [MInst, fault] ← DecodeMbusCommand[]; 
         IF MCMD AND MInst = MapOpDone THEN EXIT
         ENDLOOP}; 
    
    DecodeMbusCommand: PROC RETURNS [MInst: DragonCache.MbusCommand, fault: BOOLEAN] = {
      WITH b: NARROW[SakuraRT.Get[MDataIn], REF DragonCache.MbusType]↑ SELECT FROM 
        Instruction => {MInst ← b.command; MRP ← b.rp; MBL ← b.bl; MWord ← b.word; 
                        fault ← FALSE};
        MapCommand => {MInst ← b.command; fault ← b.fault}
        ENDCASE => ERROR}; 
    
    WaitOneCycle: PROC = {
      SakuraRT.GetNew[ClockB, TRUE]; NULL; 
      SakuraRT.GetNew[ClockA, TRUE]; NULL}; 
    
    ReadDataFromBus: PROC [data: POINTER TO LONG CARDINAL] = {
      WITH b: NARROW[SakuraRT.Get[MDataIn], REF DragonCache.MbusType]↑ SELECT FROM 
        Data => data↑ ← b.data
        ENDCASE => ERROR}; 
    
    ArbiterInterface: PROC = {
      arbiterHolding: BOOLEAN ← FALSE;
      {ENABLE {ABORTED => GO TO Aborted};
       DO SakuraRT.GetNew[ClockA, TRUE]; NULL; 
          SakuraRT.Delay[15]; 
          IF NOT arbiterHolding AND (PRq OR MRq) 
             THEN {arbiterHolding ← TRUE; 
                   SakuraRT.Put[Rq, NEW[BOOLEAN ← TRUE]]} 
             ELSE IF arbiterHolding AND NOT PRq AND NOT MRq THEN 
                     {arbiterHolding ← FALSE; 
                      SakuraRT.Put[Rq, NEW[BOOLEAN ← FALSE]]}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; 
    
    -- Back door operations
    
    BackDoor: PROC = {
      MInst: DragonCache.MbusCommand;
      {ENABLE {ABORTED => GO TO Aborted};
       DO SakuraRT.GetNew[ClockB, TRUE]; NULL; 
          MCMD ← NARROW[SakuraRT.Get[CMDIn], REF BOOLEAN]↑; 
          IF MCMD THEN 
             {[MInst, ] ← DecodeMbusCommand[]; 
              SELECT MInst FROM 
                ReadQuad => BDReadQuad[];
                WriteQuad => NULL;
                WriteSingle => BDWriteSingle[];
                ReadMap => NULL;
                ReadMapAndSetRpDirty => BDReadMapAndSetRpDirty[];
                SetRpDirty => BDSetRpDirty[];
                DoMapOp => NULL
                ENDCASE}
          ENDLOOP; 
       SakuraRT.ProcessEnd[]}
      EXITS
        Aborted => SakuraRT.Abort[]}; 
    
    BDReadQuad: PROC = {
      -- Starts in B
      index: CARDINAL; 
      success: BOOLEAN; 
      ReadOneWord: PROC = {
        SakuraRT.GetNew[ClockB, TRUE]; IF success THEN MWData ← Data[index].D[MWord]; 
        SakuraRT.GetNew[ClockA, TRUE];
         {IF success THEN 
             SakuraRT.Put[MDataOut, NEW[DragonCache.MbusType ← [Data[MWData]]]]; 
          MWord ← (MWord + 1) MOD 4}};
      SakuraRT.GetNew[ClockA, TRUE]; [success, index] ← FullRpMatch[MRP, MBL]; 
      IF success THEN 
         {Data[index].Shared ← TRUE; 
          SakuraRT.Put[SharedOut, NEW[BOOLEAN ← TRUE]]}; 
      SakuraRT.GetNew[ClockB, TRUE]; NULL; 
      THROUGH [1..4] DO
          ReadOneWord[]
          ENDLOOP; 
      SakuraRT.GetNew[ClockB, TRUE]; SakuraRT.Put[SharedOut, NEW[BOOLEAN ← FALSE]]}; 
    -- BDReadQuad
    
    BDWriteSingle: PROC = {
      index: CARDINAL; 
      success: BOOLEAN;
      SakuraRT.GetNew[ClockA, TRUE]; [success, index] ← FullRpMatch[MRP, MBL]; 
      SakuraRT.Delay[30]; 
      ReadDataFromBus[@MRdData]; --  (A)
      SakuraRT.GetNew[ClockB, TRUE]; IF success THEN 
                                        Data[index].D[MWord] ← MRdData}; 
    -- BDWriteSingle
    
    BDReadMapAndSetRpDirty: PROC = {
      index: CARDINAL; 
      success: BOOLEAN;
      SakuraRT.GetNew[ClockA, TRUE]; [success, index] ← FullRpMatch[MRP, MBL]; 
      SakuraRT.GetNew[ClockB, TRUE]; IF success THEN Data[index].RpDirty ← TRUE}; 
    -- BDReadMapAndSetRpDirty
    
    BDSetRpDirty: PROC = {
      index: CARDINAL; 
      success: BOOLEAN;
      SakuraRT.GetNew[ClockA, TRUE]; [success, index] ← FullRpMatch[MRP, MBL]; 
      SakuraRT.GetNew[ClockB, TRUE]; IF success THEN Data[index].RpDirty ← TRUE};
    -- BDSetRpDirty
    
    {ENABLE {ABORTED => GO TO Aborted};
     SakuraRT.Put[Reject, NEW[BOOLEAN ← FALSE]]; 
     SakuraRT.Put[SharedOut, NEW[BOOLEAN ← FALSE]]; 
     SakuraRT.Put[CMDOut, NEW[BOOLEAN ← FALSE]]; 
     
     FOR i: CARDINAL IN [0..DataArraySize) DO
         Data[i].VpValid ← Data[i].RpValid ← FALSE
         ENDLOOP; 
     SakuraRT.GetNew[ClockA, TRUE]; NULL; 
     
     {pbus, fetch, store, domapop, mproc, backdoor, arbinterface: PROCESS; 
      SakuraRT.IncCurrent[];pbus ← FORK PbusFetch;SakuraRT.CatalogProcId[pbus]; 
      SakuraRT.IncCurrent[];fetch ← FORK FetchTransport;SakuraRT.CatalogProcId[fetch]; 
      SakuraRT.IncCurrent[];store ← FORK StoreTransport;SakuraRT.CatalogProcId[store]; 
      SakuraRT.IncCurrent[];
      domapop ← FORK DoMapOpTransport;SakuraRT.CatalogProcId[domapop]; 
      SakuraRT.IncCurrent[];mproc ← FORK MProc;SakuraRT.CatalogProcId[mproc]; 
      SakuraRT.IncCurrent[];backdoor ← FORK BackDoor;SakuraRT.CatalogProcId[backdoor]; 
      SakuraRT.IncCurrent[];
      arbinterface ← FORK ArbiterInterface;SakuraRT.CatalogProcId[arbinterface]; 
      SakuraRT.DecCurrent[]; 
      SakuraRT.Join[pbus]; 
      SakuraRT.Join[fetch]; 
      SakuraRT.Join[store]; 
      SakuraRT.Join[domapop]; 
      SakuraRT.Join[mproc]; 
      SakuraRT.Join[backdoor]; 
      SakuraRT.Join[arbinterface]; 
      SakuraRT.IncCurrent[]}; 
     SakuraRT.ProcessEnd[]}
    EXITS
      Aborted => SakuraRT.Abort[]}; 
  

  -- Data array access procedures
  
  FullVpMatch: PROC [vp: LONG CARDINAL, bl: CARDINAL] RETURNS [BOOLEAN, CARDINAL] = {
    FOR i: CARDINAL IN [0..DataArraySize) DO
        IF Data[i].VpValid AND Data[i].vp = vp AND Data[i].bl = bl THEN 
           RETURN [TRUE, i]
        ENDLOOP; 
    RETURN [FALSE, 0]}; 
  
  FullRpMatch: PROC [rp: LONG CARDINAL, bl: CARDINAL] RETURNS [BOOLEAN, CARDINAL] = {
    FOR i: CARDINAL IN [0..DataArraySize) DO
        IF Data[i].RpValid AND Data[i].rp = rp AND Data[i].bl = bl THEN 
           RETURN [TRUE, i]
        ENDLOOP; 
    RETURN [FALSE, 0]}; 
  
  PartialMatch: ENTRY PROC [vp: LONG CARDINAL] RETURNS [BOOLEAN, CARDINAL] = {
    FOR i: CARDINAL IN [0..DataArraySize) DO
        IF Data[i].VpValid AND Data[i].vp = vp THEN 
           {RpDirtyReg ← Data[i].RpDirty; 
            RETURN [TRUE, i]}
        ENDLOOP; 
    RETURN [FALSE, 0]};
  
  END.