module StableReset where import Array import List import Maybe infixr 5 <||> type Link = Int struct NullNetWork struct NetWork a < NullNetWork = send' :: Link -> a -> Action struct NullClient struct NWClient a < NullClient = receive :: Link -> a -> Action struct PolledClient a < NWClient a = poll :: Link -> Request (Maybe a) struct Periodic = tick :: Link -> Action struct PeriodicClient a < PolledClient a, Periodic struct StabilizableClient a s < PolledClient a = current_state :: Link -> Request s check_invariants :: Link -> s -> Request Bool local_reset :: Link -> Action data StablePkt a s = DataPkt a | RequestPkt Int SnapMode | ResponsePkt Int SnapMode s data SnapMode = Snap | Reset deriving Eq stabilizer :: Int -> Array Link Bool -> StabilizableClient a s -> NullNetWork -> Template (NullNetWork,PeriodicClient (StablePkt a s)) stabilizer dim leader client network = template checking := array (1,dim) False count := array (1,dim) 0 mode := array (1,dim) Snap in let tick i = action checking!i := True poll i = request if checking!i then if leader!i then return (Just (RequestPkt (count!i) (mode!i))) else if mode!i == Reset then client.local_reset i s <- client.current_state i checking!i := False mode!i := Snap return (Just (ResponsePkt (count!i) (mode!i) s)) else m <- client.poll i return (map DataPkt m) receive i (DataPkt m) = client.receive i m receive i (RequestPkt c m) = action if not (leader!i) then checking!i := True count!i := c mode!i := m receive i (ResponsePkt c m s) = action if checking!i && leader!i && count!i == c then count!i := (count!i + 1) `mod` 4 if mode!i == Snap then ok <- client.check_invariants i s if not ok then mode!i := Reset else checking!i := False else client.local_reset i checking!i := False in (struct ..NullNetWork, struct ..PeriodicClient) ----------------------------------------------------------------------- type Layer hi ho li lo = (ho,lo) -> Template (hi,li) (<|||>) :: Layer hi ho mi mo -> Layer mo mi li lo -> Layer hi ho li lo {- ta <|||> tb = \(ho,lo) -> fst `map` fixM (\(_,mo) -> do (hi,mi) <- ta (ho,mo) (mo,li) <- tb (mi,lo) return ((hi,li),mo)) -} ta <|||> tb = \(ho,lo) -> do fix (hi,mi) <- ta (ho,mo) (mo,li) <- tb (mi,lo) return (hi,li) ta <||> tb = \client network -> do fix (a_up,a_down) <- ta client b_up (b_up,b_down) <- tb a_down network return (a_up,b_down) {- ta <||> tb = \client network -> do (a_up,a_down,b_up,b_down) <- fixM (\(_,_,b_up',_) -> do (a_up,a_down) <- ta client b_up' (b_up,b_down) <- tb a_down network return (a_up,a_down,b_up,b_down)) return (a_up,b_down) -} timer :: Int -> Periodic -> Action timer = undefined stabilizer' dim leader client network = do s <- stabilizer dim leader client network timer 500 (snd s) return s stabilize proto dim leader = proto dim <||> stabilizer dim leader stabilize' proto dim leader = proto dim <||> stabilizer' dim leader ------------------------------------------------------------------------ struct Resettable = reset :: Action struct ResetNetWork a < NetWork a, Resettable struct ResetClient a < NWClient a, Resettable data ResetMsg a = DataMsg a | AbortMsg Int | AckMsg | ReadyMsg instance Eq (ResetMsg a) where DataMsg _ == DataMsg _ = True AbortMsg d == AbortMsg d' = d == d' AckMsg == AckMsg = True ReadyMsg == ReadyMsg = True _ == _ = False data ResetMode = AbortMode | ConvergeMode | ReadyMode deriving Eq --global_reset :: Int -> ResetClient a -> NullNetWork -> -- Template (ResetNetWork a, StabilizableClient (ResetMsg a) LocalState) global_reset dim client network = template ack_pend := [] parent := Nothing distance := 0 buffer := array (1,dim) [] queue := array (1,dim) [] in let mode [] Nothing = ReadyMode mode [] (Just _) = ConvergeMode mode _ _ = AbortMode send' i m = action if mode ack_pend parent == ReadyMode then enqueue i (DataMsg m) enqueue i m = do queue!i := queue!i ++ [m] poll i = request case queue!i of m:ms -> queue!i := ms return (Just m) [] -> return Nothing receive i m = action do_receive i m do_receive i (DataMsg m) = do if mode ack_pend parent == ReadyMode then client.receive i m else buffer!i := buffer!i ++ [m] do_receive i (AbortMsg dist) = do if mode ack_pend parent == ReadyMode then propagate (Just i) dist if dist == 0 || mode ack_pend parent /= ReadyMode then enqueue i AckMsg buffer!i := [] do_receive i AckMsg = do if i `elem` ack_pend then ack_pend := delete i ack_pend case mode ack_pend parent of ConvergeMode -> enqueue (the parent) AckMsg ReadyMode -> reset_completed AbortMode -> done do_receive i ReadyMsg = do if mode ack_pend parent == ConvergeMode && parent == Just i then parent := Nothing reset_completed reset_completed = do client.reset forall j <- [1..dim] do enqueue j ReadyMsg forall i <- [1..dim] do forall m <- buffer!i do client.receive i m buffer!i := [] propagate par dist = do parent := if dist /= 0 then par else Nothing distance := dist forall j <- [1..dim] do enqueue j (AbortMsg (distance+1)) ack_pend := [1..dim] reset = action propagate Nothing 0 ---------------------- current_state i = request return (struct mode = mode ack_pend parent you_parent = parent == Just i ack_in_q = AckMsg `elem` queue!i rdy_in_q = ReadyMsg `elem` queue!i you_pending = i `elem` ack_pend distance = distance) check_invariants i remote = request let p0 = i `elem` ack_pend p1 = AbortMsg (distance+1) `elem` queue!i p2 = remote.mode == AbortMode && remote.you_parent p3 = remote.ack_in_q p4 = parent == Just i p5 = mode ack_pend parent == ConvergeMode p6 = AckMsg `elem` queue!i p7 = not remote.you_pending && remote.mode /= ReadyMode p8 = remote.rdy_in_q p9 = f1 (queue!i) p10 = mode ack_pend parent == ReadyMode p11 = distance == remote.distance + 1 f1 [] = False f1 [ReadyMsg] = True f1 [DataMsg _] = True f1 (m:ms) = f1 ms f2 [AbortMsg _,AckMsg] = True f2 [AckMsg,ReadyMsg,AbortMsg _] = True f2 [ReadyMsg,AbortMsg _] = True f2 (AckMsg:ReadyMsg:ms) = f3 ms f2 (ReadyMsg:ms) = f3 ms f2 ms = f3 ms f3 [] = True f3 (DataMsg _:ms) = f3 ms f3 _ = False pA = p0 == (p1 || p2 || p3) pB = length (filter id [p1,p2,p3]) <= 1 pC = (p4 `implies` p5) == (p6 || p7 || p8) pD = length (filter id [p6,p7,p8]) <= 1 pR = p9 `implies` p10 pP = p4 `implies` (p11 || p8) pQ = f2 (queue!i) False `implies` _ = True True `implies` a = a return (pA && pB && pC && pD && pR && pP && pQ) local_reset i = action do_receive i AckMsg do_receive i ReadyMsg if parent == Just i then parent := Nothing buffer!i := [] queue!i := [] in (struct ..ResetNetWork, struct ..StabilizableClient) struct LocalState = mode :: ResetMode you_parent :: Bool ack_in_q :: Bool rdy_in_q :: Bool you_pending :: Bool distance :: Int ---------------------------------------------------------------------- struct HWNetWork < NullNetWork struct HWClient < NullClient udl :: Int -> PolledClient a -> HWNetWork -> Template (NullNetWork,HWClient) udl = undefined n = 5 leader = array (1,n) True stable_global_reset = stabilize global_reset n leader stable_global_reset' = stabilize' global_reset n leader stack = stable_global_reset <||> udl n stack' = global_reset n <||> udl n stack'' = stabilizer' n leader <||> udl n