# Theory BufferExample

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

section ‹Buffer example›

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

where
[(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
```