cache experiment

package.yaml

@@ -140,6 +140,7 @@ library:
     - Memory.Vec
     - Memory.ST
     - Memory.IO
+    - Memory.Cache
     - Leak.Arch.Arch
     - Leak.PC.ISA
     - Leak.PC.Leak

proof-smt/Proof/Functional/Induction.hs

@@ -69,7 +69,8 @@ data KState = KState
     kWbRes :: Word,
     kCtrl :: Core.Control Identity,
     kHalt :: Maybe Core.HaltState,
-    kHaltNextPc :: Address
+    kHaltNextPc :: Address,
+    kLoadInFlight :: Bool
   }
 
 -- | Assemble a system state from the symbolic pieces.
@@ -90,7 +91,8 @@ sysOf ss i ra ma =
             Core.stateRegFile = RegArrF ra,
             Core.stateCtrl = kCtrl ss,
             Core.stateHalt = kHalt ss,
-            Core.stateHaltNextPc = kHaltNextPc ss
+            Core.stateHaltNextPc = kHaltNextPc ss,
+            Core.stateLoadInFlight = kLoadInFlight ss
           },
       sysInput = i,
       sysMem = ma

proof/Proof/Leakage/Simulator.hs

@@ -94,9 +94,10 @@ censor sys@(Sys st inp _) =
               stateRegFile = initRFg,
               stateCtrl = initCtrl,
               stateHalt = stateHalt st,
-              stateHaltNextPc = stateHaltNextPc st
+              stateHaltNextPc = stateHaltNextPc st,
+              stateLoadInFlight = stateLoadInFlight st
             },
-        sysInput = Input (inputIsInstr inp) (Identity 0),
+        sysInput = Input (inputIsInstr inp) (Identity 0) True,
         sysMem = ()
       }
 
@@ -196,7 +197,7 @@ scrub l (Sys st inp _) =
               stateRegFile = initRFg,
               stateCtrl = initCtrl
             },
-        sysInput = Input (inputIsInstr inp) (Identity 0),
+        sysInput = Input (inputIsInstr inp) (Identity 0) True,
         sysMem = ()
       }
   where
@@ -276,9 +277,9 @@ stepSimOut w (Sys s i _) =
   let (s', o) = Core.circuit s i
       i' = case getFirst (outMem o) of
         Just (MemAccess isInstr _ _ Nothing) ->
-          Input isInstr (Identity (if isInstr then w else 0))
-        Just (MemAccess isInstr _ _ (Just _)) -> Input isInstr (Identity 0)
-        Nothing -> Input False (Identity 0)
+          Input isInstr (Identity (if isInstr then w else 0)) True
+        Just (MemAccess isInstr _ _ (Just _)) -> Input isInstr (Identity 0) True
+        Nothing -> Input False (Identity 0) True
    in (Sys s' i' (), o)
 
 -- | Put the leaked instruction word on the simulator's bus.
@@ -290,7 +291,7 @@ stepSimOut w (Sys s i _) =
 -- later through 'stepSimOut'.
 installLeak :: Word -> SimSys r -> SimSys r
 installLeak word (Sys s i m)
-  | inputIsInstr i = Sys s (Input True (Identity word)) m
+  | inputIsInstr i = Sys s (Input True (Identity word) True) m
   | otherwise = Sys s i m
 
 -- | The implementation, run for one driver hop, with the observation of each

proof/Proof/Machine.hs

@@ -24,6 +24,11 @@
     isNopInstr,
     isBubble,
     readMemWord,
+    CacheSys (..),
+    initCacheSys,
+    stepCached,
+    stepCachedOut,
+    stepCachedN,
   )
 where
 
@@ -33,10 +38,11 @@
 import Data.Maybe (isNothing)
 import Data.Monoid (getFirst)
 import Instruction
+import Memory.Cache (CacheOps (..))
 import Memory.Types
 import RegFile
 import Types
 import qualified Types
 import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||))
 
 -- | Core state, the input it is about to consume, and memory.
@@ -83,10 +89,10 @@
         -- A read. Note 'Memory.Vec.ramRead' ignores the size and always reads a
         -- word; the size-dependent narrowing happens in 'Core.writeback' via
         -- 'loadExtend'. We reproduce that here.
-        Nothing -> (Input isInstr (pure (memReadWord addr mem)), mem)
+        Nothing -> (Input isInstr (pure (memReadWord addr mem)) True, mem)
         -- A write.
-        Just val -> (Input isInstr (pure 0), memWriteWord size addr (runIdentity val) mem)
-    service Nothing mem = (Input False (pure 0), mem)
+        Just val -> (Input isInstr (pure 0) True, memWriteWord size addr (runIdentity val) mem)
+    service Nothing mem = (Input False (pure 0) True, mem)
 
 stepSysN :: (RegFileOps r, MemOps m) => Int -> SysG r m -> SysG r m
 stepSysN n s
@@ -126,3 +132,49 @@
 
 readMemWord :: Address -> MemBytes -> Word
 readMemWord = readWord
+
+-- | System state paired with a cache model.
+data CacheSys r m c = CacheSys
+  { cacheSysCore :: SysG r m,
+    cacheSysCache :: c,
+    -- | Address and remaining cycles for a pending load miss.
+    cacheSysPending :: Maybe (Address, Int)
+  }
+
+deriving instance (Show (r Identity), Show m, Show c) => Show (CacheSys r m c)
+
+initCacheSys :: SysG r m -> c -> CacheSys r m c
+initCacheSys sys cache = CacheSys sys cache Nothing
+
+-- | Step a system with memory serviced through a cache.
+stepCached :: (RegFileOps r, MemOps m, CacheOps c) => Int -> CacheSys r m c -> CacheSys r m c
+stepCached missPenalty = fst . stepCachedOut missPenalty
+
+stepCachedOut ::
+  (RegFileOps r, MemOps m, CacheOps c) =>
+  Int ->
+  CacheSys r m c ->
+  (CacheSys r m c, Output Identity)
+stepCachedOut missPenalty (CacheSys (Sys s i m) cache pending) =
+  let (s', o) = Core.circuit s i
+      (i', m', cache', pending') = respond (getFirst (outMem o)) m cache pending
+   in (CacheSys (Sys s' i' m') cache' pending', o)
+  where
+    respond mAccess mem c (Just (addr, n))
+      | n > 0 = (Input False (pure 0) False, mem, c, Just (addr, n - 1))
+      | otherwise =
+          let w = memReadWord addr mem
+           in (Input False (pure w) True, mem, cacheInsert addr w c, Nothing)
+    respond Nothing mem c Nothing = (Input False (pure 0) True, mem, c, Nothing)
+    respond (Just (MemAccess isInstr addr size mval)) mem c Nothing = case mval of
+      Just val ->
+        (Input isInstr (pure 0) True, memWriteWord size addr (runIdentity val) mem, cacheInvalidate addr c, Nothing)
+      Nothing | isInstr -> (Input isInstr (pure (memReadWord addr mem)) True, mem, c, Nothing)
+      Nothing -> case cacheLookup addr c of
+        Just w -> (Input isInstr (pure w) True, mem, c, Nothing)
+        Nothing -> (Input isInstr (pure 0) False, mem, c, Just (addr, missPenalty - 1))
+
+stepCachedN :: (RegFileOps r, MemOps m, CacheOps c) => Int -> Int -> CacheSys r m c -> CacheSys r m c
+stepCachedN missPenalty n s
+  | n <= 0 = s
+  | otherwise = stepCachedN missPenalty (n - 1) (stepCached missPenalty s)

src/Core.hs

@@ -61,7 +61,9 @@ data Input f = Input
   { -- | Is this an instruction read?
     inputIsInstr :: Bool,
     -- | Reads from memory.
-    inputMem :: f Word
+    inputMem :: f Word,
+    -- | Is the memory answer ready this cycle?
+    inputMemReady :: Bool
   }
 
 deriving instance (Show (f Word)) => Show (Input f)
@@ -143,7 +145,9 @@ data StateG r f = State
     -- | CPU halt state.
     stateHalt :: Maybe HaltState,
     -- | In case of a halt, the address of the next instruction.
-    stateHaltNextPc :: Address
+    stateHaltNextPc :: Address,
+    -- | True when a load is in flight.
+    stateLoadInFlight :: Bool
   }
 
 -- | The synthesisable state: the register file is a 'Vec'.
@@ -186,7 +190,9 @@ data Control f = Control
     ctrlMeRegFwd :: Maybe (RegIdx, f Word),
     -- | Forwards the `rd` register from the `writeback` stage to the `execute`
     -- stage.
-    ctrlWbRegFwd :: Maybe (RegIdx, f Word)
+    ctrlWbRegFwd :: Maybe (RegIdx, f Word),
+    -- | True when a load was in flight at the start of the cycle.
+    ctrlMeHadInFlight :: Bool
   }
 
 deriving instance (Show (f Word)) => Show (Control f)
@@ -224,7 +230,8 @@ initInput :: (Access f) => Input f
 initInput =
   Input
     { inputIsInstr = False,
-      inputMem = pure 0
+      inputMem = pure 0,
+      inputMemReady = True
     }
 
 init :: forall f r. (Access f, RegFileOps r) => StateG r f
@@ -242,7 +249,8 @@ init =
       stateRegFile = initRFg,
       stateCtrl = initCtrl,
       stateHalt = Nothing,
-      stateHaltNextPc = 0
+      stateHaltNextPc = 0,
+      stateLoadInFlight = False
     }
 
 -- | Initial control lines.
@@ -257,7 +265,8 @@ initCtrl =
       ctrlMeMemInstr = False,
       ctrlMeStoreAddrSize = Nothing,
       ctrlMeRegFwd = Nothing,
-      ctrlWbRegFwd = Nothing
+      ctrlWbRegFwd = Nothing,
+      ctrlMeHadInFlight = False
     }
 
 -- | The control lines need to be reset every tick.
@@ -281,7 +290,7 @@ fetch = do
   -- Always try to read unless the instruction in the `memory` stage is a load or a store.
   unless (ctrlMeMemInstr ctrl) $
     readPC pc
-  
+
   -- We stall if the instruction in the `memory` stage is a load or a store.
   let stall = ctrlMeMemInstr ctrl
 
@@ -304,10 +313,15 @@ fetch = do
 -- | Decode stage.
 decode :: (Access f) => CPUM r f ()
 decode = do
+  hadInFlight <- gets (ctrlMeHadInFlight . stateCtrl)
+  unless hadInFlight decodeFresh
+
+decodeFresh :: (Access f) => CPUM r f ()
+decodeFresh = do
   input <- ask
   pc <- gets stateDePc
   ctrl <- gets stateCtrl
-  
+
   ir <-
     if inputIsInstr input
       then noSecrets' (inputMem input) (Nop Halted) (pure . decode')
@@ -362,6 +376,11 @@ decode = do
 -- | Execute stage.
 execute :: forall f r. (Access f, RegFileOps r) => CPUM r f ()
 execute = do
+  hadInFlight <- gets (ctrlMeHadInFlight . stateCtrl)
+  unless hadInFlight execute'
+
+execute' :: forall f r. (Access f, RegFileOps r) => CPUM r f ()
+execute' = do
   ir <- gets stateExInstr
 
   -- Default values.
@@ -525,8 +544,18 @@ branch op lhs rhs = case op of
   where
     sign = unpack @(Signed 32)
 
+-- | Memory stage.
 memory :: CPUM r f ()
 memory = do
+  wasInFlight <- gets stateLoadInFlight
+  setLines $ \c -> c {ctrlMeHadInFlight = wasInFlight}
+  if wasInFlight
+    then setLines $ \c -> c {ctrlMeMemInstr = True}
+    else memoryFresh
+
+-- | Process a fresh memory instruction.
+memoryFresh :: CPUM r f ()
+memoryFresh = do
   ir <- gets stateMeInstr
   res <- gets stateMeRes
   addr <- gets stateMeAddr
@@ -544,6 +573,7 @@ memory = do
     Instruction.IType (Load size _) _ _ _ -> do
       setLines $ \c -> c {ctrlMeMemInstr = True}
       readRAM addr size
+      modify $ \s -> s {stateLoadInFlight = True}
     Instruction.SType size _ _ _ -> do
       setLines $ \c ->
         c {ctrlMeMemInstr = True, ctrlMeStoreAddrSize = Just (addr, size)}
@@ -559,9 +589,8 @@ memory = do
 -- | Commit computations to the register file.
 writeback :: forall f r. (Access f, RegFileOps r) => CPUM r f ()
 writeback = do
-  input <- asks inputMem
   ir <- gets stateWbInstr
-  res <- gets stateWbRes  
+  res <- gets stateWbRes
 
   case ir of
     Instruction.RType _ rd _ _ -> do
@@ -571,9 +600,13 @@ writeback = do
       setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)}
       writeRF rd res
     Instruction.IType (Load size sign) rd _ _ -> do
-      let val = loadExtend size sign <$> input
-      setLines $ \c -> c {ctrlWbRegFwd = Just (rd, val)}
-      writeRF rd val
+      ready <- asks inputMemReady
+      when ready $ do
+        input <- asks inputMem
+        let val = loadExtend size sign <$> input
+        setLines $ \c -> c {ctrlWbRegFwd = Just (rd, val)}
+        writeRF rd val
+        modify $ \s -> s {stateLoadInFlight = False}
     Instruction.JType rd _ -> do
       setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)}
       writeRF rd res

src/HardwareSim.hs

@@ -40,6 +40,7 @@
             ( fromMaybe False $ memIsInstr <$> getFirst (outMem o)
             )
             (Identity mread)
+            True
       )
         <$> cpuOut
         <*> ram
@@ -78,7 +79,7 @@
       imap (\(i :: Index n) _ -> v !! idx i) (repeat undefined)
       where
         off :: Int
         off = fromIntegral (snatToNum offset)
 
         idx :: Index n -> Index ((GHC.TypeNats.*) n 4)
         idx i = fromInteger (toInteger off + toInteger i * 4)