CSPによる並行システムの検証その２

阪大での講義のスライドとサンプルコードを公開する。前回→CSPによるコンカレントシステムの検証(1)

スライド

サンプルコード

OS.csp

enum {l, m, h, none};

var active = none;

var wait_h = false;
var wait_m = false;
var wait_l = false;

H = [active == h](act_h -> H [] act_h{wait_h = false} -> H);
M = [active == m](act_m -> M [] act_m{wait_m = false} -> M);
L = [active == l](act_l -> L [] act_l{wait_l = false} -> L);

Scheduler =
 atomic {
  (req_h -> {wait_h = true} -> Skip
  [] req_m -> {wait_m = true} -> Skip
  [] req_l -> {wait_l = true} -> Skip);
  case {
   wait_h: {active = h} -> Skip
   wait_m: {active = m} -> Skip
   wait_l: {active = l} -> Skip
   default: {active = none} -> Skip
  }
 }; Scheduler;

Env = [!wait_h]req_h -> Env [] [!wait_m]req_m -> Env [] [!wait_l]req_l -> Env;

System = H ||| M ||| L ||| (Scheduler || Env);
 
#assert System deadlockfree;

#assert System |= G(req_h -> F act_h);
#assert System |= G(req_m -> F act_m);
#assert System |= G(req_l -> F act_l);

#assert System |= G(req_h -> ((! act_l) U act_h));
#assert System |= G(req_l -> ((! act_h) U act_l));

OS-PriInv.csp

enum {l, m, h, none};

var active = none;

var wait_h = false;
var wait_m = false;
var wait_l = false;

var resource = none;

H = [active == h && (resource == none || resource == h)]
 (act_h{resource = h} -> H
  [] act_h{resource = none; wait_h = false} -> H);
M = [active == m](act_m -> M [] act_m{wait_m = false} -> M);
L = [active == l && (resource == none || resource == l)]
 (act_l{resource = l} -> L 
  [] act_l{resource = none; wait_l = false} -> L);

Scheduler =
 atomic {
  (req_h -> {wait_h = true} -> Skip
  [] req_m -> {wait_m = true} -> Skip
  [] req_l -> {wait_l = true} -> Skip);
  case {
   wait_h: {active = h} -> Skip
   wait_m: {active = m} -> Skip
   wait_l: {active = l} -> Skip
   default: {active = none} -> Skip
  }
 }; Scheduler;

Env = [!wait_h]req_h -> Env [] [!wait_m]req_m -> Env [] [!wait_l]req_l -> Env;

System = H ||| M ||| L ||| (Scheduler || Env);
 
#assert System deadlockfree;

#assert System |= G(req_h -> F act_h);
#assert System |= G(req_m -> F act_m);
#assert System |= G(req_l -> F act_l);

#assert System |= G(req_h -> ((! act_l) U act_h));
#assert System |= G(req_l -> ((! act_h) U act_l));

OS-PriInh.csp

enum {l, m, h, none};

var active = none;

var wait_h = false;
var wait_m = false;
var wait_l = false;

var resource = none;

H = [active == h && (resource == none || resource == h)]
 (act_h{resource = h} -> H
  [] act_h{resource = none; wait_h = false} -> H);
M = [active == m](act_m -> M [] act_m{wait_m = false} -> M);
L = [active == l && (resource == none || resource == l)]
 (act_l{resource = l} -> L 
  [] act_l{resource = none; wait_l = false} -> L);

Scheduler =
 atomic {
  (req_h -> {wait_h = true} -> Skip
  [] req_m -> {wait_m = true} -> Skip
  [] req_l -> {wait_l = true} -> Skip);
  case {
   resource == l: {active = l} -> Skip
   wait_h: {active = h} -> Skip
   wait_m: {active = m} -> Skip
   wait_l: {active = l} -> Skip
   default: {active = none} -> Skip
  }
 }; Scheduler;

Env = [!wait_h]req_h -> Env [] [!wait_m]req_m -> Env [] [!wait_l]req_l -> Env;

System = H ||| M ||| L ||| (Scheduler || Env);
 
#assert System deadlockfree;

#assert System |= G(req_h -> F act_h);
#assert System |= G(req_m -> F act_m);
#assert System |= G(req_l -> F act_l);

#assert System |= G(req_h -> ((! act_l) U act_h));
#assert System |= G(req_l -> ((! act_h) U act_l));