Theory BufferExample

(*  Title:      JinjaThreads/Examples/BufferExample.thy
    Author:     Andreas Lochbihler
*)

section ‹Buffer example›

theory BufferExample imports 
  "../Execute/Code_Generation"
begin

definition ThreadC :: "addr J_mb cdecl"
where 
  "ThreadC = 
  (Thread, Object, [], 
    [(run, [], Void, ⌊([], unit)⌋),
     (start, [], Void, Native),
     (join, [], Void, Native),
     (interrupt, [], Void, Native),
     (isInterrupted, [], Boolean, Native)])"

definition IntegerC :: "addr J_mb cdecl"
where "IntegerC = (STR ''Integer'', Object, [(STR ''value'', Integer, ⦇volatile=False⦈)], [])"

definition Buffer :: cname
where "Buffer = STR ''Buffer''"

definition BufferC :: "addr J_mb cdecl"
where
  "BufferC =
   (Buffer, Object,
    [(STR ''buffer'', Class Object⌊⌉, ⦇volatile=False⦈),
     (STR ''front'', Integer, ⦇volatile=False⦈),
     (STR ''back'', Integer, ⦇volatile=False⦈),
     (STR ''size'', Integer, ⦇volatile=False⦈)],
    [(STR ''constructor'', [Integer], Void, ⌊([STR ''size''],
      (STR ''buffer'' := newA (Class Object)⌊Var (STR ''size'')⌉);;
      (STR ''front'' := Val (Intg 0));;
      (STR ''back'' := Val (Intg (- 1)));;
      (Var this∙(STR ''size''){STR ''''} := Val (Intg 0)))⌋),
     (STR ''empty'', [], Boolean, ⌊([], sync(Var this) (Var (STR ''size'') «Eq» Val (Intg 0)))⌋),
     (STR ''full'', [], Boolean, ⌊([],
      sync(Var this) (Var (STR ''size'') «Eq» ((Var (STR ''buffer''))∙length)))⌋),
     (STR ''get'', [], Class Object, ⌊([],
      sync(Var this) (
        (while (Var this∙(STR ''empty'')([])) 
          (try (Var this∙wait([])) catch(InterruptedException (STR ''e'')) unit));;
        (STR ''size'' := (Var (STR ''size'') «Subtract» Val (Intg 1)));;
        {(STR ''result''):Class Object=None; 
          ((STR ''result'') := ((Var (STR ''buffer''))⌊Var (STR ''front'')⌉));;
          (STR ''front'' := (Var (STR ''front'') «Add» Val (Intg 1)));;
          (if ((Var (STR ''front'')) «Eq» ((Var (STR ''buffer''))∙length))
             (STR ''front'' := Val (Intg 0))
           else unit);;
          (Var this∙notifyAll([]));;
          Var (STR ''result'')
        }
      ))⌋),
     (STR ''put'', [Class Object], Void, ⌊([STR ''o''],
      sync(Var this) (
        (while (Var this∙STR ''full''([]))
          (try (Var this∙wait([])) catch(InterruptedException STR ''e'') unit));;
        (STR ''back'' := (Var (STR ''back'') «Add» Val (Intg 1)));;
        (if (Var (STR ''back'') «Eq» ((Var (STR ''buffer''))∙length))
           (STR ''back'' := Val (Intg 0))
         else unit);;
        (AAss (Var (STR ''buffer'')) (Var (STR ''back'')) (Var (STR ''o'')));;
        (STR ''size'' := ((Var (STR ''size'')) «Add» Val (Intg 1)));;
        (Var this∙notifyAll([]))
      ))⌋)
    ])"

definition Producer :: cname
where "Producer = STR ''Producer''"

definition ProducerC :: "int ⇒ addr J_mb cdecl"
where
  "ProducerC n =
   (Producer, Thread, [(STR ''buffer'', Class Buffer, ⦇volatile=False⦈)],
    [(run, [], Void, ⌊([],
     {STR ''i'':Integer=⌊Intg 0⌋;
        while (Var (STR ''i'') «NotEq» Val (Intg (word_of_int n))) (
          (Var (STR ''buffer''))∙STR ''put''([{STR ''temp'':Class (STR ''Integer'')=None; (STR ''temp'' := new (STR ''Integer'');; ((FAss (Var (STR ''temp'')) (STR ''value'') (STR '''') (Var (STR ''i'')));; Var (STR ''temp'')))} ]);;
          STR ''i'' := (Var (STR ''i'') «Add» (Val (Intg 1))))
     })⌋)])"

definition Consumer :: cname
where "Consumer = STR ''Consumer''"

definition ConsumerC :: "int ⇒ addr J_mb cdecl"
where
  "ConsumerC n =
  (Consumer, Thread, [(STR ''buffer'', Class Buffer, ⦇volatile=False⦈)],
   [(run, [], Void, ⌊([],
    {STR ''i'':Integer=⌊Intg 0⌋;
      while (Var (STR ''i'') «NotEq» Val (Intg (word_of_int n))) (
        {STR ''o'':Class Object=None; 
          Seq (STR ''o'' := ((Var (STR ''buffer''))∙STR ''get''([])))
              (STR ''i'' := (Var (STR ''i'') «Add» Val (Intg 1)))})
    })⌋)])"

definition String :: cname
where "String = STR ''String''"

definition StringC :: "addr J_mb cdecl"
where
  "StringC = (String, Object, [], [])"

definition Test :: cname
where "Test = STR ''Test''"

definition TestC :: "addr J_mb cdecl"
where
  "TestC =
  (Test, Object, [],
   [(STR ''main'', [Class String⌊⌉], Void, ⌊([STR ''args''], 
    {STR ''b'':Class Buffer=None; (STR ''b'' := new Buffer);;
      (Var (STR ''b'')∙STR ''constructor''([Val (Intg 10)]));;
      {STR ''p'':Class Producer=None; STR ''p'' := new Producer;;
        {STR ''c'':Class Consumer=None; 
           (STR ''c'' := new Consumer);;
           (Var (STR ''c'')∙STR ''buffer''{STR ''''} := Var (STR ''b''));;
           (Var (STR ''p'')∙STR ''buffer''{STR ''''} := Var (STR ''b''));;
           (Var (STR ''c'')∙Type.start([]));;(Var (STR ''p'')∙Type.start([]))
        }
      }
    })⌋)])"
    
definition BufferExample
where
  "BufferExample n = Program (SystemClasses @ [ThreadC, StringC, IntegerC, BufferC, ProducerC n, ConsumerC n, TestC])"

definition BufferExample_annotated
where
  "BufferExample_annotated n = annotate_prog_code (BufferExample n)"

lemmas [code_unfold] =
  IntegerC_def Buffer_def Producer_def Consumer_def Test_def
  String_def

lemma "wf_J_prog (BufferExample_annotated 10)"
by eval

definition main where "main = STR ''main''"
definition five :: int where "five = 5"

ML_val ‹
  val program = @{code BufferExample_annotated} @{code "five"};
  val compiled = @{code J2JVM} program;

  val run = 
    @{code exec_J_rr}
      @{code "1 :: nat"}
      program
      @{code Test}
      @{code main}
      [ @{code Null}];
  val _ = @{code terminal} run;

  val jvm_run = 
    @{code exec_JVM_rr} 
      @{code "1 :: nat"}
      compiled
      @{code Test}
      @{code main}
      [ @{code Null}];
  val _ = @{code terminal} run;
›

end