強化学習シリーズの途中ですが、BSVの例題を見つけたので、紹介します。

「哲学者の食事」をBSVでシミュレーションするものです。

一度にスプーンは片手で1つしか持てず、2つ取ろうとすると、右手⇒左手、もしくは左手→右手の順にスプーンを取るしかありません。ここで、全員が右手⇒左手のように取ると、全員が右手に1つを持ったまま、左側のスプーンが空くのを永久に待つことになり、いわゆるデッドロックが起きます。

ソースは一人の哲学者が他人とは反対の順で取るようにプログラムしてあり、それにより全員がなんらかの形で食事をすることができる様子を示しています。

ソースコード

//
// CBG SQUANDERER : Dining Philosophers In Bluespec
// (C) 2012 David Greaves, University of Cambridge

import StmtFSM::*;

interface Spoon_if;
   method Action pickup;
   method Action putdown;
endinterface

(* synthesize *)
module spoon (Spoon_if) ;
   Reg#(Bool) inuse <- mkReg(?);
   method Action pickup if (!inuse);
     inuse <= True;
   endmethod
   method Action putdown;
     inuse <= False;
   endmethod
endmodule

(* synthesize *)
module philoBENCH (Empty) ;
   Spoon_if spoon0 <- spoon; 
   Spoon_if spoon1 <- spoon; 
   Spoon_if spoon2 <- spoon; 
   Spoon_if spoon3 <- spoon; 
   Spoon_if spoon4 <- spoon; 
   Diner_if din0 <- mkDiner (7, 7, spoon1, spoon0); // <---- Reverse pickup
   Diner_if din1 <- mkDiner (6, 4, spoon1, spoon2);
   Diner_if din2 <- mkDiner (5, 9, spoon2, spoon3);
   Diner_if din3 <- mkDiner (6, 6, spoon3, spoon4);
   Diner_if din4 <- mkDiner (8, 8, spoon4, spoon0);
   Reg#(UInt#(15)) timer <- mkReg(5000);
   rule foo;
      timer <= timer - 1;
      if (timer == 0) $finish;
   endrule
endmodule: philoBENCH

interface Random_if;
   method ActionValue#(UInt#(15)) gen;
endinterface    

module mkRandom_gen #(UInt#(15) seed) (Random_if);
   Reg#(UInt#(15)) prbs <- mkReg(seed);
   method ActionValue#(UInt#(15)) gen;
      prbs <= (prbs << 1) | (((prbs >> 14) ^ (prbs >> 13)) & 1);   
      return prbs;
  endmethod
endmodule 

interface Diner_if;
endinterface

module mkDiner #(UInt#(15) on, UInt#(15) seed) (Spoon_if left, Spoon_if right, Diner_if i) ;
   Reg#(Bool) eating <- mkReg(?);    
   Reg#(UInt#(15)) timer <- mkReg(0);
   Random_if random <- mkRandom_gen(seed);
   rule foo (timer != 0);
      timer <= timer - 1;
   endrule
   Stmt seq_behaviour = (seq
      while (True) seq
         action
            UInt#(15) x <- random.gen;
            timer <= x & 31;
         endaction
         await(timer== 0);
         left.pickup;
         action
            UInt#(15) x <- random.gen;
            timer <= x & 31;
         endaction
         await(timer== 0);
         right.pickup;
         action
            eating <= True;
            timer <= on;
         endaction
         await(timer==0);
         eating <= False;
         left.putdown; 
         right.putdown;
      endseq
   endseq);
   mkAutoFSM(seq_behaviour);
endmodule

前のブログ 次のブログ