-- File: [Indigo]<Sakura>Dragon>DragonCacheControlImpl.sak
-- Dragon Cache
-- 18-Feb-82 15:50:59

DIRECTORY
  DragonCacheControl: TYPE, 
  Inline: TYPE, 
  SakuraRT: TYPE;

DragonCacheImpl: MONITOR
  IMPORTS Inline, SakuraRT
  EXPORTS DragonCacheControl
  
  -- 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.
  
  -- i) Fetch
  --Match on Pbus
  --IF success THEN Fetch
  --ELSE {
  --  IF Victim dirty THEN WriteQuad Victim;
  --  Partial Match on Pbus
  --  IF ~ success THEN ReadMap;
  --  ReadQuad};
  
  --ii) Store
  --Match on Pbus
  --IF success THEN
  --  IF ~Shared THEN
  --    IF RpDirty THEN Store to Ram
  --    ELSE {SetRpDirty; Store to Ram}
  --  ELSE 
  --    IF RpDirty THEN WriteSingle
  --    ELSE {SetRpDirty; WriteSingle}
  --ELSE {
  --  IF Victim dirty THEN WriteQuad Victim;
  --  PartialMatch;
  --  IF ~success THEN ReadMap;
  --  ReadQuad;
  --  GO TO ii) Store}
  
  = 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]; 
  PbusType: TYPE = 
    RECORD [body: SELECT kind: {Instruction, Data} FROM 
                    Instruction => [vp: LONG CARDINAL, -- actually 25 bits -- 
                                    bl: INTEGER [0..37B], 
                                    word: INTEGER [0..3]],
                    Data => [data: LONG CARDINAL]
                    ENDCASE]; 
  MbusType: TYPE = 
    RECORD [body: SELECT kind: {Instruction, MapCommand, Data} FROM 
                    Instruction => [command: MbusCommand, 
                                    rp: LONG CARDINAL, -- actually 25 bits -- 
                                    bl: INTEGER [0..37B], 
                                    word: INTEGER [0..3]],
                    MapCommand => [command: MbusCommand, 
                                   mapop: MapOpKind, 
                                   fault: BOOLEAN, 
                                   vp: LONG CARDINAL],
                    Data => [data: LONG CARDINAL]
                    ENDCASE]; 
  MbusCommand: TYPE = {ReadQuad, WriteQuad, WriteSingle, NotReady, ReadMap, 
                       DoMapOp, SetRpDirty, SetRpDirtyDone}; 
  MapOpKind: TYPE = {SetMap, SetMapFlags, GetMapFlags}; 
  MProcType: TYPE = PROC; 
  
  -- Constants
  DataArraySize: CARDINAL = 64; 
  
  -- Global variables
  FetchTransportGo, StoreTransportGo, DoMapOpTransportGo, Grant, Holding, MShared, 
  DoMProc, MProcDone, PRq, NewRq, MRq, Orph, MCMD: BOOLEAN; 
  Instruction, Reqbus: {Fetch, FetchHold, Store, MapOp, Noop}; 
  DataIndex, VictimIndex: CARDINAL; 
  RqVP, MVP: LONG CARDINAL; 
  RqBL, PBL, MBL: INTEGER [0..37B]; 
  RqData: LONG CARDINAL; 
  PWord, MWord: INTEGER [0..3]; 
  PResult: LONG CARDINAL; 
  PRP, MRP: LONG CARDINAL; 
  Pbus: PbusType; 
  Mbus: MbusType; 
  Data: ARRAY INTEGER [0..DataArraySize) OF Cell; 
  MOp: MProcType; 
  MOResult: LONG CARDINAL; 
  MRdData: LONG CARDINAL; 
  MWData: LONG CARDINAL; 
  MInst: MbusCommand; 
  MapOp: MapOpKind; 
  

  PageFault: SIGNAL = CODE; 
  WriteViolation: SIGNAL = CODE; 
  


  Cache: PUBLIC PROC
       [PDataIn, MDataIn: SakuraRT.Handle, CMDIn, RQ, SharedIn: SakuraRT.Handle, 
        Exception, Reject, SharedOut, CMDOut: SakuraRT.Handle, 
        PDataOut, MDataOut: SakuraRT.Handle] = {
    

    -- PbusFetch process procedures
    
    PbusFetch: PROC = {
      success: BOOLEAN;
      DO --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: Pbus SELECT FROM 
               Instruction => {RqVP _ b.vp; RqBL _ b.bl; PWord _ b.word}
               ENDCASE => ERROR; 
             Instruction _ Reqbus; 
             --M (Phase B)
             [success, DataIndex] _ FullMatch[RqVP, RqBL]; 
             {ENABLE {
                PageFault => 
                  {Pbus _ [Data[-1]]; SakuraRT.Put[Exception, NEW[BOOLEAN _ TRUE]]};
                WriteViolation => 
                  {Pbus _ [Data[0]]; SakuraRT.Put[Exception, NEW[BOOLEAN _ TRUE]]}};
              SELECT Instruction FROM 
                Fetch => CallFetch[];
                FetchHold => 
                  CallFetchHold
                    [! PageFault => 
                         {Pbus _ [Data[-1]]; Holding _ FALSE; 
                          SakuraRT.Put[Exception, NEW[BOOLEAN _ TRUE]]};
                       WriteViolation => 
                         {Pbus _ [Data[0]]; SakuraRT.Put[Exception, NEW[BOOLEAN _ TRUE]]}];
                Store => CallStore[];
                MapOp => CallMapOp[];
                Noop => NULL
                ENDCASE}}
         ENDLOOP}; 
    
    CallFetch: PROC = {
      success: BOOLEAN;
      -- Started at Phase B
      IF success --hit
         THEN {SakuraRT.Put[Reject, NEW[BOOLEAN _ FALSE]]; 
               FetchTransportGo _ TRUE; 
               Holding _ FALSE} 
         ELSE {SakuraRT.Put[Reject, NEW[BOOLEAN _ TRUE]]; 
               Holding _ FALSE; 
               --R (Phase A)
               Holding _ TRUE; 
               --T (Phase B)
               PRq _ TRUE; 
               WaitForGrant[]; 
               WriteBackVictimIfDirty[]; 
               [success, PRP] _ PartialMatch[RqVP]; 
               --Clock (Phase B)
               IF NOT success THEN CallMProc[ReadMap]; 
               CallMProc[ReadQuad]; 
               PRq _ FALSE; 
               SakuraRT.Put[Reject, NEW[BOOLEAN _ FALSE]]; 
               [success, DataIndex] _ FullMatch[RqVP, RqBL]; 
               IF NOT success THEN ERROR; -- This is a description error
               FetchTransportGo _ TRUE}}; 
    
    CallFetchHold: PROC = {
      -- Started at Phase B
      IF NOT Holding THEN 
         {SakuraRT.Put[Reject, NEW[BOOLEAN _ TRUE]]; 
          PRq _ TRUE; 
          WaitForGrant[]; 
          --Clock (Phase B)
          Holding _ TRUE}; 
      CallFetch[]}; 
    
    CallStore: PROC = {
      success: BOOLEAN;
      SakuraRT.Put[Reject, NEW[BOOLEAN _ TRUE]]; 
      -- Clock (A)
      WITH b: Pbus SELECT FROM 
        Data => RqData _ b.data
        ENDCASE => ERROR; 
      IF NOT success THEN 
         {PRq _ TRUE; 
          WaitForGrant[]; 
          WriteBackVictimIfDirty[]; 
          --Clock (Phase B)
          [success, PRP] _ PartialMatch[RqVP]; 
          IF NOT success THEN CallMProc[ReadMap]; 
          --Clock (Phase B)
          CallMProc[ReadQuad]}; 
      --Clock (B)
      [success, DataIndex] _ FullMatch[RqVP, RqBL]; 
      IF NOT Data[DataIndex].Shared 
         THEN {IF NOT Data[DataIndex].RpDirty THEN CallMProc[SetRpDirty]; 
               SakuraRT.Put[Reject, NEW[BOOLEAN _ FALSE]]; 
               StoreTransportGo _ TRUE} 
         ELSE {IF NOT Data[DataIndex].RpDirty THEN CallMProc[SetRpDirty]; 
               Data[DataIndex].D[PWord] _ RqData; 
               CallMProc[WriteSingle]}; 
      PRq _ FALSE}; -- CallStore
    
    CallMapOp: PROC = {
      -- Started at Phase B
      SakuraRT.Put[Reject, NEW[BOOLEAN _ TRUE]]; 
      PRq _ TRUE; 
      WaitForGrant[]; 
      -- Clock (A)
      WITH b: Pbus SELECT FROM 
        Data => RqData _ b.data
        ENDCASE => ERROR; 
      CallMProc[DoMapOp]; 
      PRq _ FALSE}; -- CallMapOp
    
    CallMProc: PROC [procedure: MProcType] = {
      -- Starts in Phase B and finishes in Phase B
      MProcDone _ FALSE; 
      DoMProc _ TRUE; 
      MOp _ procedure; 
      DO --Clock (Phase A)
         IF MProcDone THEN EXIT
         ENDLOOP}; -- CallMProc
    
    WriteBackVictimIfDirty: PROC = {
      -- Starts at Phase A
      MRP _ Data[VictimIndex].rp; 
      MBL _ Data[VictimIndex].bl; 
      IF Data[VictimIndex].CEDirty THEN 
         {CallMProc[WriteQuad]; 
          Data[VictimIndex].CEDirty _ FALSE}}; -- WriteBackVictimIfNotClean
    
    WaitForGrant: PROC = {
      DO --Clock (Phase A)
         IF Grant THEN EXIT
         ENDLOOP}; -- WaitForGrant
    


    -- FetchTransport process procedures
    
    FetchTransport: PROC = {
      -- Starts at Phase A
      DO --R (Phase A)
         IF FetchTransportGo THEN 
            {PResult _ Data[DataIndex].D[PWord]; 
             FetchTransportGo _ FALSE; 
             --T (Phase B)
             Pbus _ [Data[PResult]]}
         ENDLOOP}; 
    
    StoreTransport: PROC = {
      -- Starts at Phase A
      DO --clock (A)
         IF StoreTransportGo THEN 
            {Data[DataIndex].D[PWord] _ RqData; 
             StoreTransportGo _ FALSE}
         ENDLOOP}; -- StoreTransport
    
    DoMapOpTransport: PROC = {
      DO -- clock (B)
         IF DoMapOpTransportGo THEN 
            {NewRq _ TRUE; 
             MOResult _ MRdData; 
             SakuraRT.Put[Reject, NEW[BOOLEAN _ FALSE]]; 
             --clock (A)
             PResult _ MOResult; 
             NewRq _ FALSE; 
             -- clock (B)
             IF Inline.BITAND[Inline.HighHalf[PResult], 40000B] # 0 THEN 
                SakuraRT.Put[Exception, NEW[BOOLEAN _ TRUE]]; 
             Pbus _ [Data[PResult]]}
         ENDLOOP}; -- DoMapOpTransport
    


    -- MProc process procedures
    
    MProc: PROC = {DO --Clock (Phase A)
                      MProcDone _ FALSE; 
                      IF DoMProc THEN 
                         {DoMProc _ FALSE; 
                          MOp[]}
                      ENDLOOP}; 
    
    WriteQuad: PROC = {
      i: CARDINAL; 
      WriteOneWord: PROC [pword: INTEGER [0..3]] = {
        --Clock (Phase B)
        MWData _ Data[DataIndex].D[pword]; 
        --Clock (Phase A)
        Mbus _ [Data[MWData]]}; -- WriteOneWord
      --Clock (Phase A)
      Mbus _ [Instruction[WriteQuad, MRP, MBL, 0]]; 
      FOR i IN [0..3] DO
          WriteOneWord[i]
          ENDLOOP; 
      MProcDone _ TRUE}; -- WriteQuad
    
    ReadMap: PROC = {
      fault: BOOLEAN;
      --Clock (Phase A)
      Mbus _ [MapCommand[ReadMap, , , MVP]]; 
      fault _ WaitMapOpDone[]; 
      IF fault THEN SIGNAL PageFault; 
      MProcDone _ TRUE}; 
    
    ReadQuad: PROC = {
      ReadOneWord: PROC = {IF NOT Orph THEN ReadDataFromBus[@Data[DataIndex].D[PWord]]}; 
      success: BOOLEAN;
      --Clock (Phase A)
      Mbus _ [Instruction[ReadQuad, PRP, PBL, PWord]]; 
      WITH b: Mbus SELECT FROM 
        Instruction => {MRP _ b.rp; MBL _ b.bl; MWord _ b.word}
        ENDCASE => ERROR; 
      --Clock (Phase B, t2)
      MRq _ TRUE; 
      --Clock (Phase A, t3)
      [success, DataIndex] _ FullMatch[MRP, MBL]; 
      --Clock (Phase B, t4)
      Orph _ success; 
      IF NOT success THEN DataIndex _ VictimIndex; 
      --Clock (Phase A, t5)
      IF NOT success THEN 
         {Data[DataIndex].rp _ MRP; 
          Data[DataIndex].bl _ MBL}; 
      --Clock (Phase B, t6)
      Data[DataIndex].vp _ RqVP; 
      Data[DataIndex].Shared _ NARROW[SakuraRT.Get[SharedIn], REF BOOLEAN]^; 
      VictimIndex _ (VictimIndex + 1) MOD DataArraySize; 
      --Clock (Phase A, t7)
      MCMD _ NARROW[SakuraRT.Get[CMDIn], REF BOOLEAN]^; 
      ReadOneWord[]; 
      IF MCMD AND MInst = NotReady THEN WaitOneCycle[]; 
      MProcDone _ TRUE; 
      --Clock (Phase B, t8)
      ReadOneWord[]; 
      --Clock (Phase A, t9)
      PWord _ (PWord + 1) MOD 4; 
      --Clock (Phase B, t10)
      Data[DataIndex].TIP _ TRUE; 
      ReadOneWord[]; 
      MRq _ FALSE; 
      IF NOT Holding THEN NewRq _ TRUE; 
      --Clock (Phase A, t11)
      PWord _ (PWord + 1) MOD 4; 
      --Clock (Phase B, t12)
      ReadOneWord[]; 
      IF NOT Holding THEN NewRq _ FALSE; 
      --Clock (Phase A, t13)
      PWord _ (PWord + 1) MOD 4; 
      --Clock (Phase B, t14)
      ReadOneWord[]; 
      Data[DataIndex].TIP _ FALSE}; 
    
    SetRpDirty: PROC = {
      fault: BOOLEAN;
      --Clock (Phase A)
      Mbus _ [Instruction[SetRpDirty, PRP, PBL, PWord]]; 
      WITH b: Mbus SELECT FROM 
        Instruction => 
          {MRP _ b.rp; 
           MBL _ b.bl; 
           MWord _ b.word}
        ENDCASE => ERROR; 
      --Clock (Phase B)
      fault _ WaitMapOpDone[]; 
      IF fault THEN SIGNAL WriteViolation; 
      MProcDone _ TRUE}; 
    
    WriteSingle: PROC = {
      --Clock (Phase A)
      Mbus _ [Instruction[WriteSingle, PRP, PBL, PWord]]; 
      NewRq _ TRUE; 
      --Clock (Phase B)
      MWData _ Data[DataIndex].D[PWord]; 
      --Clock (Phase A)
      Mbus _ [Data[MWData]]; 
      MProcDone _ TRUE; 
      NewRq _ FALSE}; 
    
    DoMapOp: PROC = {
      fault: BOOLEAN;
      --Clock (Phase A)
      Mbus _ [MapCommand[DoMapOp, MapOp, , MVP]]; 
      MCMD _ TRUE; 
      --Clock (Phase B)
      MWData _ RqData; 
      --Clock (Phase A)
      Mbus _ [Data[MWData]]; 
      fault _ WaitMapOpDone[]; 
      IF fault THEN SIGNAL PageFault; 
      MProcDone _ TRUE; 
      ReadDataFromBus[@MRdData]; 
      DoMapOpTransportGo _ TRUE}; -- DoMapOp
    
    WaitMapOpDone: PROC RETURNS [fault: BOOLEAN] = {
      DO --Clock (Phase A)
         MCMD _ NARROW[SakuraRT.Get[CMDIn], REF BOOLEAN]^; 
         [MInst, fault] _ DecodeMbusCommand[]; 
         IF MCMD AND MInst = SetRpDirtyDone THEN EXIT
         ENDLOOP}; 
    
    DecodeMbusCommand: PROC RETURNS [MInst: MbusCommand, fault: BOOLEAN] = {
      WITH b: Mbus SELECT FROM 
        MapCommand => {MInst _ b.command; fault _ b.fault}
        ENDCASE => ERROR}; 
    
    WaitOneCycle: PROC = {}; 
    --Clock (Phase B)
    --Clock (Phase A)
    


    -- Backdoor process procedures
    
    BackDoor: PROC = {
      DO -- clock (B)
         MCMD _ NARROW[SakuraRT.Get[CMDIn], REF BOOLEAN]^; 
         [MInst, ] _ DecodeMbusCommand[]; 
         IF MCMD THEN 
            SELECT MInst FROM 
              ReadQuad => BDReadQuad[];
              WriteQuad => BDWriteQuad[];
              WriteSingle => BDWriteSingle[];
              ReadMap => NULL;
              SetRpDirty => BDSetRpDirty[];
              DoMapOp => NULL
              ENDCASE
         ENDLOOP}; 
    
    BDReadQuad: PROC = {
      success: BOOLEAN; 
      ReadOneWord: PROC = {
        -- clock (B)
        IF success THEN MWData _ Data[DataIndex].D[MWord]; 
        -- clock (A)
        IF success THEN Mbus _ [Data[MWData]]; 
        MWord _ (MWord + 1) MOD 4};
      [success, DataIndex] _ FullMatch[MRP, MBL]; 
      -- clock (A)
      IF success THEN MShared _ TRUE; 
      THROUGH [1..4] DO
          ReadOneWord[]
          ENDLOOP; 
      -- clock (B)
      MShared _ FALSE}; -- BDReadQuad
    
    BDWriteQuad: PROC = {
      success: BOOLEAN; 
      WriteOneWord: PROC = {
        -- clock (B)
        IF success THEN Data[DataIndex].D[MWord] _ MRdData; 
        -- clock (A)
        MWord _ MWord + 1; 
        ReadDataFromBus[@MRdData]};
      [success, DataIndex] _ FullMatch[MRP, MBL]; 
      -- clock (A)
      IF success THEN 
         {MShared _ TRUE; MWord _ 0; 
          ReadDataFromBus[@MRdData]}; 
      THROUGH [1..3] DO
          WriteOneWord[]
          ENDLOOP; 
      -- clock (B)
      IF success THEN Data[DataIndex].D[MWord] _ MRdData; 
      IF success THEN MShared _ FALSE}; -- BDWriteQuad
    
    BDWriteSingle: PROC = {
      success: BOOLEAN;
      [success, DataIndex] _ FullMatch[MRP, MBL]; 
      -- clock (A)
      ReadDataFromBus[@MRdData]; 
      -- clock (B)
      IF success THEN Data[DataIndex].D[MWord] _ MRdData}; -- BDWriteSingle
    
    BDSetRpDirty: PROC = {
      success: BOOLEAN;
      [success, DataIndex] _ FullMatch[MRP, MBL]; 
      -- clock (A)
      -- clock (B)
      IF success THEN Data[DataIndex].RpDirty _ TRUE}; -- BDSetRpDirty
    
    ReadDataFromBus: PROC [data: POINTER TO LONG CARDINAL] = {
      WITH b: Mbus SELECT FROM 
        Data => data^ _ b.data
        ENDCASE => ERROR}; 
    


    -- Data array access procedures
    
    FullMatch: ENTRY 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]}; 
    
    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 
             RETURN [TRUE, i]
          ENDLOOP; 
      RETURN [FALSE, 0]};
    

    {ENABLE {ABORTED => GO TO Aborted};
     {st1: PROC = {{PbusFetch[]; 
                    SakuraRT.ProcessEnd[]}}; 
      st2: PROC = {{FetchTransport[]; 
                    SakuraRT.ProcessEnd[]}}; 
      st3: PROC = {{StoreTransport[]; 
                    SakuraRT.ProcessEnd[]}}; 
      st4: PROC = {{DoMapOpTransport[]; 
                    SakuraRT.ProcessEnd[]}}; 
      st5: PROC = {{MProc[]; 
                    SakuraRT.ProcessEnd[]}}; 
      process1, process2, process3, process4, process5: PROCESS; 
      process1 _ SakuraRT.Fork[st1]; 
      process2 _ SakuraRT.Fork[st2]; 
      process3 _ SakuraRT.Fork[st3]; 
      process4 _ SakuraRT.Fork[st4]; 
      process5 _ SakuraRT.Fork[st5]; 
      BackDoor[]; 
      [] _ SakuraRT.Join[process1]; 
      [] _ SakuraRT.Join[process2]; 
      [] _ SakuraRT.Join[process3]; 
      [] _ SakuraRT.Join[process4]; 
      [] _ SakuraRT.Join[process5]}; 
     SakuraRT.ProcessEnd[]}
    EXITS
      Aborted => SakuraRT.ProcessEnd[]};
  


  END.