Mercurial > hg > Papers > 2022 > soto-sigos
changeset 8:971da38e7596
ADD deadlock 検知できるようにはなった
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 May 2022 02:51:33 +0900 |
| parents | 6a61c1eb0205 |
| children | bc8222372b9d |
| files | DPP/ModelChecking.agda |
| diffstat | 1 files changed, 135 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/DPP/ModelChecking.agda Thu May 12 15:44:39 2022 +0900 +++ b/DPP/ModelChecking.agda Mon May 23 02:51:33 2022 +0900 @@ -258,6 +258,31 @@ test11 f (s@(x ∷ x1 ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit test11 f ((x ∷ x1 ∷ x2 ∷ xs) ∷ bs) exit = {!!} +record metadata : Set where + field + num-branch : ℕ + wait-list : List ℕ +open metadata + +record MetaEnv : Set where + field + DG : List Env + meta : metadata + deadlock : Bool +open MetaEnv + + +branch-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +branch-deadlock-check metaenv exit = search-brute-force-envll-p [] metaenv exit where + search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + search-brute-force-envll-p f [] exit = exit f + search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv + ... | [] = search-brute-force-envll-p f bs exit + ... | (env ∷ envs) = brute-force-search env (λ e0 → make-brute-force-envl (length e0) [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit)) where + make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t + make-brute-force-envl len res xs [] exit = exit res + make-brute-force-envl len res xs (x ∷ state) exit = make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit + data _===_ {n} {A : Set n} : List A -> List A -> Set n where @@ -271,9 +296,83 @@ testhoge C_pickup_lfork C_pickup_lfork = {!!} testhoge _ _ = {!!} +step-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +step-deadlock-check metaenvl exit = deadlock-check-p [] metaenvl exit where + deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + deadlock-check-p f [] exit = exit f + deadlock-check-p f b@(metaenv ∷ bs) exit with DG metaenv + ... | [] = deadlock-check-p f bs exit + ... | p0 ∷ [] = deadlock-check-p f bs exit + ... | p0 ∷ bp ∷ envs = check-wait-process [] (ph p0) bp ( λ e → deadlock-check-p (f ++ (record metaenv{meta = record (meta metaenv){wait-list = e } } ∷ [])) bs exit) where + check-wait-process : {n : Level} {t : Set n} → List ℕ → List Phi → (p1 : Env) → (exit : List ℕ → t) → t + check-wait-process waitl [] p1 exit = exit waitl + check-wait-process waitl (p ∷ ps) p1 exit = hoge11 p (ph p1) (λ e → check-wait-process (waitl ++ e) ps p1 exit) where + hoge11 : {n : Level} {t : Set n} → Phi → List Phi → (exit : List ℕ → t) → t + hoge11 p [] exit = exit [] + hoge11 p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) + hoge11 p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 p p1s exit + hoge11 p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 p p1s exit + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit [] -test-step-c : (List Env) -test-step-c = brute-force-search record { +step-brute-force-meta : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +step-brute-force-meta metaenvl exit = step-brute-force-p [] metaenvl exit where + step-brute-force-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → (exit : List MetaEnv → t) → t + step-brute-force-p f [] exit = exit f + step-brute-force-p f (metaenv ∷ bs) exit with DG metaenv + ... | [] = step-brute-force-p f bs exit + ... | envl@(x ∷ xs) = step-c x (λ e0 → step-brute-force-p (f ++ (record metaenv{DG = e0 ∷ envl} ∷ [])) bs exit) + + +judge-deadlock : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +judge-deadlock metaenvl exit = judge-deadlock-p [] metaenvl exit where + judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + judge-deadlock-p f [] exit = exit f + judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv) + ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | suc zero with (DG metaenv ) + ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p)) + ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit + + + +test-env-deadlock : {n : Level} {t : Set n} → (a b : Env)→ (exit : List MetaEnv → t) → t +test-env-deadlock a b exit = test12 (ph a) (ph b) exit where + test12 : {n : Level} {t : Set n} → (a b : List Phi)→ (exit : List MetaEnv → t) → t + test12 [] b = {!!} + test12 (x ∷ a) b = {!!} + +{- + test12 : List ℕ → (a b0 b : List Phi) → List ℕ + test12 stack [] b0 b = stack + test12 stack (a ∷ as) b0 [] = test12 stack as b0 b0 + test12 stack (a ∷ as) b0 (b ∷ bs) with <-cmp (pid a) (pid b) + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri< a₁ ¬b ¬c = test12 stack al b0 bs + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri> ¬a ¬b c = test12 stack al b0 bs + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ ¬a b₁ ¬c with (next-code a) + test12 stack al@(a ∷ as) b0 (b ∷ bs) | _ | aaaa with (next-code b) + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_putdown_rfork | C_putdown_rfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_putdown_lfork | C_putdown_lfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_thinking | C_thinking = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_pickup_rfork | C_pickup_rfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_pickup_lfork | C_pickup_lfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_eating | C_eating = pid a ∷ [] + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | _ | _ = test12 stack al b0 bs +-} + +test-env : Env +test-env = (record { table = 0 ∷ 0 ∷ 0 ∷ [] ; ph = record { pid = 1 @@ -291,7 +390,40 @@ ; right-hand = false ; next-code = C_pickup_rfork } ∷ [] - } (λ e2 → e2) + }) + +exec-brute-force-meta : {n : Level} {t : Set n} → ℕ → List MetaEnv → (exit : List MetaEnv → t) → t +exec-brute-force-meta n metaenvl exit = exec-brute-force-p n metaenvl exit where + exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List MetaEnv → (exit : List MetaEnv → t) → t + exec-brute-force-p zero envll exit = exit envll + exec-brute-force-p (suc n) envll exit = branch-deadlock-check envll (λ e1 → step-brute-force-meta e1 (λ e2 → step-deadlock-check e2 (λ e3 → judge-deadlock e3 (λ e4 → exec-brute-force-p n e4 exit)))) + + +test-dead-lock : List MetaEnv +test-dead-lock = exec-brute-force-meta 3 (record + { DG = (record { + table = 0 ∷ 0 ∷ 0 ∷ [] + ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ [] + }∷ []) + ; meta = record { num-branch = zero ; wait-list = [] } + ; deadlock = false + } ∷ []) (λ e3 → e3) + test-step-c2 : List (List Env) test-step-c2 = init-brute-force (record {