Commit f4877c57 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Paul
Browse files

Further BFF example simplification.

parent 03c5649b
......@@ -41,13 +41,12 @@ typedef u64 pte_t;
//@rc::typedef pte_t ≔ bitfield<Pte>
#define PTE_TYPE_BLOCK 0
#define PTE_TYPE_PAGE 1
#define PTE_TYPE_TABLE 1
#define TY_BLOCK 0
#define TY_PAGE 1
//@rc::inlined_prelude
//@Definition pte_type_block : Z := 0.
//@Definition pte_type_page : Z := 1.
//@Definition TY_BLOCK : Z := 0.
//@Definition TY_PAGE : Z := 1.
//@rc::end
#define MAX_LEVEL 4U
......@@ -69,34 +68,29 @@ static bool pte_valid(pte_t pte) {
//@ (if bool_decide P then l else r)
//@ (at level 100, l at next level, r at next level).
//@
//@Definition svl_pte pa level attr :=
//@ let type := level = max_level - 1 ? pte_type_page : pte_type_block in
//@ zero_Pte <| pte_addr := pte_addr pa |>
//@ <| pte_valid := true |>
//@ <| pte_type := type |>
//@ <| pte_leaf_attr_lo := pte_leaf_attr_lo attr |>
//@ <| pte_leaf_attr_hi := pte_leaf_attr_hi attr |>.
//@Definition svl_pte pa lvl attr := {|
//@ pte_addr := pa.(pte_addr);
//@ pte_valid := true;
//@ pte_type := lvl = max_level - 1 ? TY_PAGE : TY_BLOCK;
//@ pte_leaf_attr_lo := attr.(pte_leaf_attr_lo);
//@ pte_leaf_attr_hi := attr.(pte_leaf_attr_hi);
//@|}.
//@rc::end
[[rc::requires("{bitfield_wf old}", "{bitfield_wf pa}", "{bitfield_wf attr}")]] // FIXME not necessary.
[[rc::parameters("p : loc", "old : Pte", "pa : Pte", "attr : Pte", "level : Z")]]
[[rc::args("p @ &own<old @ pte_t>", "pa @ pte_t", "attr @ pte_t", "level @ int<u32>")]]
[[rc::parameters("p : loc", "old : Pte", "pa : Pte", "attr : Pte", "lvl : Z")]]
[[rc::args("p @ &own<old @ pte_t>", "pa @ pte_t", "attr @ pte_t", "lvl @ int<u32>")]]
[[rc::requires("{old.(pte_valid) = false}")]]
[[rc::returns("{true} @ boolean<bool_it>")]]
[[rc::ensures("own p : {svl_pte pa level attr} @ bitfield<Pte>")]]
static bool set_valid_leaf_pte(pte_t *ptep, u64 pa, pte_t attr, u32 level) {
[[rc::ensures("own p : {svl_pte pa lvl attr} @ bitfield<Pte>")]]
static bool set_valid_leaf_pte(pte_t *ptep, u64 pa, pte_t attr, u32 lvl) {
pte_t old = *ptep;
pte_t pte = pa & PTE_ADDR_MASK; // Inlined function.
u64 type = (level == MAX_LEVEL - 1) ?
PTE_TYPE_PAGE :
PTE_TYPE_BLOCK;
u64 type = (lvl == MAX_LEVEL - 1) ? TY_PAGE : TY_BLOCK;
pte |= attr & (PTE_LEAF_ATTR_LO | PTE_LEAF_ATTR_HI);
pte |= FIELD_PREP(PTE_TYPE, type);
pte |= PTE_VALID;
if(pte_valid(old))
return old == pte;
*ptep = pte; // smp_store_release(ptep, pte);
return true;
if(pte_valid(old)) { return old == pte; }
else { *ptep = pte; return true; } // removed smp_store_release.
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment