Library mcertikos.proc.PAbQueueCode
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import CalRealProcModule.
Require Import CommonTactic.
Require Import XOmega.
Require Import AbstractDataType.
Require Import PAbQueue.
Require Import AbQueueAtomicGenSpec.
Require Import PAbQueueCSource.
Module PAbQueueCode.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section ENQUEUE_ATOMIC.
Let L: compatlayer (cdata RData) :=
acquire_lock_TCB ↦ gensem acquire_lock_ABTCB_spec
⊕ release_lock_TCB ↦ gensem release_lock_ABTCB_spec
⊕ enqueue ↦ gensem enqueue0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section EnqueueAtomicBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bacquire_lock_TCB: block.
Hypothesis hacquire_lock_TCB1 : Genv.find_symbol ge acquire_lock_TCB = Some bacquire_lock_TCB.
Hypothesis hacquire_lock_TCB2 :
Genv.find_funct_ptr ge bacquire_lock_TCB =
Some (External (EF_external acquire_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable brelease_lock_TCB: block.
Hypothesis hrelease_lock_TCB1 : Genv.find_symbol ge release_lock_TCB = Some brelease_lock_TCB.
Hypothesis hrelease_lock_TCB2 :
Genv.find_funct_ptr ge brelease_lock_TCB =
Some (External (EF_external release_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable benqueue: block.
Hypothesis henqueue1 : Genv.find_symbol ge enqueue = Some benqueue.
Hypothesis henqueue2 :
Genv.find_funct_ptr ge benqueue =
Some (External (EF_external enqueue
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma enqueue_atomic_body_correct: ∀ m d d´ env le n i,
env = PTree.empty _ →
PTree.get _n le = Some (Vint n) →
PTree.get _i le = Some (Vint i) →
high_level_invariant d →
enqueue_atomic_spec (Int.unsigned n) (Int.unsigned i) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) enqueue_atomic_body E0 le´ (m, d´) Out_normal.
Proof.
intros m d d´ env le n i Henv Hn Hi Hinv Hspec.
generalize max_unsigned_val; intros muval.
unfold enqueue_atomic_body.
functional inversion Hspec; subst; simpl.
esplit.
repeat vcgen.
Qed.
End EnqueueAtomicBody.
Theorem enqueue_atomic_code_correct:
spec_le (enqueue_atomic ↦ enqueue_atomic_spec_low) (〚enqueue_atomic ↦ f_enqueue_atomic 〛L).
Proof.
fbigstep_pre L.
fbigstep (enqueue_atomic_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_enqueue_atomic)
(Vint n :: Vint i :: nil)
(create_undef_temps (fn_temps f_enqueue_atomic)))) H0.
Qed.
End ENQUEUE_ATOMIC.
Section DEQUEUE_ATOMIC.
Let L: compatlayer (cdata RData) :=
acquire_lock_TCB ↦ gensem acquire_lock_ABTCB_spec
⊕ release_lock_TCB ↦ gensem release_lock_ABTCB_spec
⊕ dequeue ↦ gensem dequeue0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section DequeueAtomicBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bacquire_lock_TCB: block.
Hypothesis hacquire_lock_TCB1 : Genv.find_symbol ge acquire_lock_TCB = Some bacquire_lock_TCB.
Hypothesis hacquire_lock_TCB2 :
Genv.find_funct_ptr ge bacquire_lock_TCB =
Some (External (EF_external acquire_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable brelease_lock_TCB: block.
Hypothesis hrelease_lock_TCB1 : Genv.find_symbol ge release_lock_TCB = Some brelease_lock_TCB.
Hypothesis hrelease_lock_TCB2 :
Genv.find_funct_ptr ge brelease_lock_TCB =
Some (External (EF_external release_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable bdequeue: block.
Hypothesis hdequeue1 : Genv.find_symbol ge dequeue = Some bdequeue.
Hypothesis hdequeue2 :
Genv.find_funct_ptr ge bdequeue =
Some (External (EF_external dequeue
(signature_of_type (Tcons tint Tnil) tuint cc_default))
(Tcons tint Tnil) tuint cc_default).
Lemma dequeue_atomic_body_correct: ∀ m d d´ env le n i,
env = PTree.empty _ →
PTree.get _n le = Some (Vint n) →
high_level_invariant d →
dequeue_atomic_spec (Int.unsigned n) d = Some (d´, Int.unsigned i) →
∃ le´,
exec_stmt ge env le ((m, d): mem) dequeue_atomic_body E0 le´ (m, d´)
(Out_return (Some (Vint i, tint))).
Proof.
intros m d d´ env le n i Henv Hn Hinv Hspec.
generalize max_unsigned_val; intros muval.
unfold dequeue_atomic_body.
functional inversion Hspec; subst; simpl.
esplit.
repeat vcgen.
Qed.
End DequeueAtomicBody.
Theorem dequeue_atomic_code_correct:
spec_le (dequeue_atomic ↦ dequeue_atomic_spec_low) (〚dequeue_atomic ↦ f_dequeue_atomic 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (dequeue_atomic_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_dequeue_atomic)
(Vint n :: nil)
(create_undef_temps (fn_temps f_dequeue_atomic)))) H0.
Qed.
End DEQUEUE_ATOMIC.
End WithPrimitives.
End PAbQueueCode.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import CalRealProcModule.
Require Import CommonTactic.
Require Import XOmega.
Require Import AbstractDataType.
Require Import PAbQueue.
Require Import AbQueueAtomicGenSpec.
Require Import PAbQueueCSource.
Module PAbQueueCode.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section ENQUEUE_ATOMIC.
Let L: compatlayer (cdata RData) :=
acquire_lock_TCB ↦ gensem acquire_lock_ABTCB_spec
⊕ release_lock_TCB ↦ gensem release_lock_ABTCB_spec
⊕ enqueue ↦ gensem enqueue0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section EnqueueAtomicBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bacquire_lock_TCB: block.
Hypothesis hacquire_lock_TCB1 : Genv.find_symbol ge acquire_lock_TCB = Some bacquire_lock_TCB.
Hypothesis hacquire_lock_TCB2 :
Genv.find_funct_ptr ge bacquire_lock_TCB =
Some (External (EF_external acquire_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable brelease_lock_TCB: block.
Hypothesis hrelease_lock_TCB1 : Genv.find_symbol ge release_lock_TCB = Some brelease_lock_TCB.
Hypothesis hrelease_lock_TCB2 :
Genv.find_funct_ptr ge brelease_lock_TCB =
Some (External (EF_external release_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable benqueue: block.
Hypothesis henqueue1 : Genv.find_symbol ge enqueue = Some benqueue.
Hypothesis henqueue2 :
Genv.find_funct_ptr ge benqueue =
Some (External (EF_external enqueue
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma enqueue_atomic_body_correct: ∀ m d d´ env le n i,
env = PTree.empty _ →
PTree.get _n le = Some (Vint n) →
PTree.get _i le = Some (Vint i) →
high_level_invariant d →
enqueue_atomic_spec (Int.unsigned n) (Int.unsigned i) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) enqueue_atomic_body E0 le´ (m, d´) Out_normal.
Proof.
intros m d d´ env le n i Henv Hn Hi Hinv Hspec.
generalize max_unsigned_val; intros muval.
unfold enqueue_atomic_body.
functional inversion Hspec; subst; simpl.
esplit.
repeat vcgen.
Qed.
End EnqueueAtomicBody.
Theorem enqueue_atomic_code_correct:
spec_le (enqueue_atomic ↦ enqueue_atomic_spec_low) (〚enqueue_atomic ↦ f_enqueue_atomic 〛L).
Proof.
fbigstep_pre L.
fbigstep (enqueue_atomic_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_enqueue_atomic)
(Vint n :: Vint i :: nil)
(create_undef_temps (fn_temps f_enqueue_atomic)))) H0.
Qed.
End ENQUEUE_ATOMIC.
Section DEQUEUE_ATOMIC.
Let L: compatlayer (cdata RData) :=
acquire_lock_TCB ↦ gensem acquire_lock_ABTCB_spec
⊕ release_lock_TCB ↦ gensem release_lock_ABTCB_spec
⊕ dequeue ↦ gensem dequeue0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section DequeueAtomicBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bacquire_lock_TCB: block.
Hypothesis hacquire_lock_TCB1 : Genv.find_symbol ge acquire_lock_TCB = Some bacquire_lock_TCB.
Hypothesis hacquire_lock_TCB2 :
Genv.find_funct_ptr ge bacquire_lock_TCB =
Some (External (EF_external acquire_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable brelease_lock_TCB: block.
Hypothesis hrelease_lock_TCB1 : Genv.find_symbol ge release_lock_TCB = Some brelease_lock_TCB.
Hypothesis hrelease_lock_TCB2 :
Genv.find_funct_ptr ge brelease_lock_TCB =
Some (External (EF_external release_lock_TCB
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable bdequeue: block.
Hypothesis hdequeue1 : Genv.find_symbol ge dequeue = Some bdequeue.
Hypothesis hdequeue2 :
Genv.find_funct_ptr ge bdequeue =
Some (External (EF_external dequeue
(signature_of_type (Tcons tint Tnil) tuint cc_default))
(Tcons tint Tnil) tuint cc_default).
Lemma dequeue_atomic_body_correct: ∀ m d d´ env le n i,
env = PTree.empty _ →
PTree.get _n le = Some (Vint n) →
high_level_invariant d →
dequeue_atomic_spec (Int.unsigned n) d = Some (d´, Int.unsigned i) →
∃ le´,
exec_stmt ge env le ((m, d): mem) dequeue_atomic_body E0 le´ (m, d´)
(Out_return (Some (Vint i, tint))).
Proof.
intros m d d´ env le n i Henv Hn Hinv Hspec.
generalize max_unsigned_val; intros muval.
unfold dequeue_atomic_body.
functional inversion Hspec; subst; simpl.
esplit.
repeat vcgen.
Qed.
End DequeueAtomicBody.
Theorem dequeue_atomic_code_correct:
spec_le (dequeue_atomic ↦ dequeue_atomic_spec_low) (〚dequeue_atomic ↦ f_dequeue_atomic 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (dequeue_atomic_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_dequeue_atomic)
(Vint n :: nil)
(create_undef_temps (fn_temps f_dequeue_atomic)))) H0.
Qed.
End DEQUEUE_ATOMIC.
End WithPrimitives.
End PAbQueueCode.