-
Notifications
You must be signed in to change notification settings - Fork 1
/
rvic_set_flag.v
44 lines (39 loc) · 1.66 KB
/
rvic_set_flag.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Local Open Scope Z_scope.
Section Spec.
Definition rvic_set_flag_spec (intid: Z64) (bitmap: Pointer) (adt: RData) : option RData :=
match intid with
| VZ64 intid =>
rely is_int64 intid;
let idx := intid / 64 in
let bit := intid mod 64 in
let slot := offset bitmap in
rely prop_dec (0 <= slot < 16);
rely prop_dec (0 <= idx < 512);
when gidx == ((buffer (priv adt)) @ slot);
let gn := (gs (share adt)) @ gidx in
rely g_tag (ginfo gn) =? GRANULE_STATE_REC;
rely prop_dec (glock gn = Some CPU_ID);
let gn := (gs (share adt)) @ gidx in
rely g_tag (ginfo gn) =? GRANULE_STATE_REC;
rely prop_dec (glock gn = Some CPU_ID);
if peq (base bitmap) rvic_pending_loc then
let bits := (r_pending_bits (g_rvic (gnorm gn))) @ idx in
let bits' := Z.lor bits (Z.shiftl 1 bit) in
let rvic' := (g_rvic (gnorm gn)) {r_pending_bits: (r_pending_bits (g_rvic (gnorm gn))) # idx == bits'} in
let g' := gn {gnorm: (gnorm gn) {g_rvic: rvic'}} in
Some adt {share: (share adt) {gs: (gs (share adt)) # gidx == g'}}
else
let bits := (r_mask_bits (g_rvic (gnorm gn))) @ idx in
let bits' := Z.lor bits (Z.shiftl 1 bit) in
let rvic' := (g_rvic (gnorm gn)) {r_mask_bits: (r_mask_bits (g_rvic (gnorm gn))) # idx == bits'} in
let g' := gn {gnorm: (gnorm gn) {g_rvic: rvic'}} in
Some adt {share: (share adt) {gs: (gs (share adt)) # gidx == g'}}
end.
End Spec.