[herd,asl,vmsa] Hardware management of the access flag

Very slow... Uses a lot of memory...

asllib/Interpreter.ml

@@ -974,7 +974,7 @@ module Make (B : Backend.S) (C : Config) = struct
     (* Begin EvalSRepeat *)
     | S_Repeat (body, e, _limit) ->
         let*> env1 = eval_block env body in
-        let env2 = IEnv.tick_push_bis env1 in
+        let env2 = IEnv.tick_push_bis env1 1 in
         eval_loop false env2 e body |: SemanticsRule.SRepeat
     (* End *)
     (* Begin EvalSFor *)
@@ -984,7 +984,7 @@ module Make (B : Backend.S) (C : Config) = struct
         (* By typing *)
         let undet = B.is_undetermined start_v || B.is_undetermined end_v in
         let*| env1 = declare_local_identifier env index_name start_v in
-        let env2 = if undet then IEnv.tick_push_bis env1 else env1 in
+        let env2 = if undet then IEnv.tick_push_bis env1 1 else env1 in
         let loop_msg =
           if undet then Printf.sprintf "for %s" index_name
           else

asllib/bitvector.ml

@@ -557,11 +557,13 @@ let ones length =
 let zero = zeros 1
 let one = ones 1
 let empty = (0, "")
+let is_zero = equal zero
 
 let is_zeros bv =
   let _length, data = remask bv in
   string_for_all (( = ) char_0) data
 
+let is_one = equal one
 let is_ones bv = length bv |> ones |> equal bv
 
 type mask = {

asllib/bitvector.mli

@@ -31,11 +31,17 @@ val length : t -> int
 (* --------------------------------------------------------------------------*)
 (** {2 Constructors} *)
 
+val zero : t
+(** A length 1 bitvector with a 0 bit inside. *)
+
+val is_zero : t -> bool
+(** zero predicate *)
+
 val one : t
 (** A length 1 bitvector with a 1 bit inside. *)
 
-val zero : t
-(** A length 1 bitvector with a 0 bit inside. *)
+val is_one : t -> bool
+(** one predicate *)
 
 val empty : t
 (** A length 0 bitvector. *)

asllib/env.ml

@@ -73,9 +73,9 @@ module RunTime (C : RunTimeConf) = struct
   (** [tick_push env] is [env] with [C.unroll] pushed on its unrolling stack. *)
   let tick_push env = set_unroll env (C.unroll :: env.local.unroll)
 
-  (** [tick_push_bis env] is [env] with [C.unroll -1] pushed on its unrolling
+  (** [tick_push_bis env k] is [env] with [C.unroll-k] pushed on its unrolling
       stack. *)
-  let tick_push_bis env = set_unroll env ((C.unroll - 1) :: env.local.unroll)
+  let tick_push_bis env k = set_unroll env ((C.unroll - k) :: env.local.unroll)
 
   (** [tick_pop env] is [env] with removed the unrolling stack first element. *)
   let tick_pop env =

asllib/env.mli

@@ -112,9 +112,9 @@ module RunTime (C : RunTimeConf) : sig
   (** Push a new unrolling counter on the stack. The associated loop will be
       unrolled [C.unroll] times. *)
 
-  val tick_push_bis : env -> env
+  val tick_push_bis : env -> int -> env
   (** Push a new unrolling counter on the stack. The associated loop will be
-      unrolled [C.unroll - 1] times. *)
+      unrolled [C.unroll - k] times. *)
 
   val tick_pop : env -> env
   (** Discards the last unrolling counter of the stack. *)

herd/AArch64ASLSem.ml

@@ -57,18 +57,21 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
         [ aarch64_iico_ctrl; aarch64_iico_data; aarch64_iico_order ]
 
     module ASLConf = struct
-      include TopConf.C
+      module C = struct
+        include TopConf.C
+        module PC = struct
+          include TopConf.C.PC
 
-      module PC = struct
-        include TopConf.C.PC
-
-        let doshow = aarch64_iico
-        let showevents = PrettyConf.AllEvents
-        let showpo = true
-        let showraw = aarch64_iico
+          let doshow = aarch64_iico
+          let showevents = PrettyConf.AllEvents
+          let showpo = true
+          let showraw = aarch64_iico
+        end
+        let variant = function Variant.ASL_AArch64 -> true | c -> variant c
       end
 
-      let variant = function Variant.ASL_AArch64 -> true | c -> variant c
+      let libfind = TopConf.C.libfind
+      let dirty = TopConf.dirty
     end
 
     module ASLS = ASLSem.Make (ASLConf)
@@ -79,7 +82,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
     module ASLTH = Test_herd.Make (ASLS.A)
 
     module MCConf = struct
-      include ASLConf
+      include ASLConf.C
 
       let byte = SZ.byte
       let dirty = TopConf.dirty
@@ -1154,12 +1157,12 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
 
     let check_event_structure model =
       let module MemConfig = struct
-        include ASLConf
+        include ASLConf.C
 
         let model = model
         let bell_model_info = None
-        let debug = ASLConf.debug.Debug_herd.barrier
-        let debug_files = ASLConf.debug.Debug_herd.files
+        let debug = ASLConf.C.debug.Debug_herd.barrier
+        let debug_files = ASLConf.C.debug.Debug_herd.files
         let showsome = true
         let skipchecks = StringSet.empty
         let strictskip = true
@@ -1287,6 +1290,6 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           | [] -> Warn.fatal "No possible ASL execution."
           | h :: t -> List.fold_left M.altT h t)
 
-    let spurious_setaf _ = assert false
+    let spurious_setaf _ = M.unitT ()
   end
 end

herd/AArch64Sem.ml

@@ -5,7 +5,8 @@
 (* Luc Maranget, INRIA Paris-Rocquencourt, France.                          *)
 (*                                                                          *)
 (* Copyright 2015-present Institut National de Recherche en Informatique et *)
-(* en Automatique, ARM Ltd and the authors. All rights reserved.            *)
+(* en Automatique, ARM Ltd and the authoes
+   rs. All rights reserved.            *)
 (*                                                                          *)
 (* This software is governed by the CeCILL-B license under French law and   *)
 (* abiding by the rules of distribution of free software. You can use,      *)
@@ -863,7 +864,7 @@ module Make
         and hd = dirty.hd proc in
         let ha = ha || hd in (* As far as we know hd => ha *)
         let mfault (_,ipte) m =
-          let open FaultType.AArch64 in
+         let open FaultType.AArch64 in
           (is_zero ipte.valid_v) >>=
             (fun c ->
               M.choiceT c

herd/ASLParseTest.ml

@@ -33,6 +33,11 @@
 
 module Make (Conf : RunTest.Config) (ModelConfig : MemCat.Config) = struct
   module ArchConfig = SemExtra.ConfigToArchConfig (Conf)
+  module Conf = struct
+    module C = Conf
+    let libfind = Conf.libfind
+    let dirty = None
+  end
   module ASLS = ASLSem.Make (Conf)
   module ASLA = ASLS.A
 
@@ -44,14 +49,14 @@ module Make (Conf : RunTest.Config) (ModelConfig : MemCat.Config) = struct
 
     let parser =
       let version =
-        if Conf.variant (Variant.ASLVersion `ASLv0) then `ASLv0 else `ASLv1
+        if Conf.C.variant (Variant.ASLVersion `ASLv0) then `ASLv0 else `ASLv1
       in
       ASLBase.asl_generic_parser version
   end
 
   module ASLM = MemCat.Make (ModelConfig) (ASLS)
-  module P = GenParser.Make (Conf) (ASLA) (ASLLexParse)
-  module X = RunTest.Make (ASLS) (P) (ASLM) (Conf)
+  module P = GenParser.Make (Conf.C) (ASLA) (ASLLexParse)
+  module X = RunTest.Make (ASLS) (P) (ASLM) (Conf.C)
 
   let run = X.run
 end

herd/ASLSem.ml

@@ -79,18 +79,20 @@ module AST = Asllib.AST
 module ASTUtils = Asllib.ASTUtils
 
 module type Config = sig
-  include Sem.Config
-
+  module C : Sem.Config
+  val dirty : DirtyBit.t option
   val libfind : string -> string
 end
 
-module Make (C : Config) = struct
+module Make (Conf : Config) = struct
   module V = ASLValue.V
 
+  let variant = Conf.C.variant
+
   module ConfLoc = struct
-    include SemExtra.ConfigToArchConfig (C)
+    include SemExtra.ConfigToArchConfig (Conf.C)
 
-    let default_to_symb = C.variant Variant.ASL
+    let default_to_symb = variant Variant.ASL
   end
 
   module ASL64AH = struct
@@ -101,26 +103,26 @@ module Make (C : Config) = struct
   end
 
   module Act = ASLAction.Make (ASL64AH)
-  include SemExtra.Make (C) (ASL64AH) (Act)
+  include SemExtra.Make (Conf.C) (ASL64AH) (Act)
 
   module TypeCheck = Asllib.Typing.Annotate (struct
     let check : Asllib.Typing.strictness =
-      if C.variant (Variant.ASLType `Warn) then `Warn
-      else if C.variant (Variant.ASLType `TypeCheck) then `TypeCheck
+      if variant (Variant.ASLType `Warn) then `Warn
+      else if variant (Variant.ASLType `TypeCheck) then `TypeCheck
       else `Silence
 
     let output_format = Asllib.Error.Silence
   end)
 
   module ASLInterpreterConfig = struct
     let unroll =
-      match C.unroll with None -> Opts.unroll_default `ASL | Some u -> u
+      match Conf.C.unroll with None -> Opts.unroll_default `ASL | Some u -> u
 
     module Instr = Asllib.Instrumentation.SemanticsNoInstr
   end
 
-  let is_experimental = C.variant Variant.ASLExperimental
-  and is_kvm = C.variant Variant.VMSA
+  let is_experimental = variant Variant.ASLExperimental
+  and is_kvm = variant Variant.VMSA
   let barriers = []
   let isync = None
   let atomic_pair_allowed _ _ = true
@@ -597,6 +599,10 @@ module Make (C : Config) = struct
         (use_ii_with_poi ii poi)
       >>! []
 
+    let write_pte ii addr_m val_m =
+      do_write_memory ii addr_m (M.unitT (V.intToV 64)) val_m
+        aneutral (AArch64Explicit.(NExp AF)) apte
+
     let write_memory ii addr_m datasize_m value_m =
       do_write_memory ii addr_m datasize_m value_m aneutral aexp avir
 
@@ -657,6 +663,14 @@ module Make (C : Config) = struct
       and loc = A.Location_global loc in
       M.mk_singleton_es (Act.Fault (ii,loc,d,ft)) ii >>! []
 
+    let get_ha (ii,_) () =
+      let dirty =
+        match Conf.dirty with
+        | None -> DirtyBit.soft
+        | Some f -> f in
+      let ha = dirty.DirtyBit.ha ii.A.proc in
+      V.Val (Constant.Concrete (ASLScalar.bv_of_bool ha)) |> M.unitT
+
     (**************************************************************************)
     (* ASL environment                                                        *)
     (**************************************************************************)
@@ -815,6 +829,9 @@ module Make (C : Config) = struct
         p3 "DataAbortPrimitive"
           ("addr",bv_64) ("write",boolean) ("statuscode",integer)
           data_abort_fault;
+        p0r "GetHaPrimitive" ~returns:(bv_lit 1) get_ha;
+        p2 "WritePtePrimitive"
+          ("addr", bv_64)  ("data",bv_64) write_pte;
 (* Translations *)
          p1r "UInt"
           ~parameters:[ ("N", None) ]
@@ -856,7 +873,7 @@ module Make (C : Config) = struct
       in
       let build ?ast_type version fname =
         Filename.concat "asl-pseudocode" fname
-        |> C.libfind
+        |> Conf.libfind
         |> ASLBase.build_ast_from_file ?ast_type version
       in
       let patches =
@@ -938,7 +955,7 @@ module Make (C : Config) = struct
       in
       fun () ->
         Lazy.force
-        @@ if C.variant Variant.ASL_AArch64 then if_asl_aarch64 else otherwise
+        @@ if variant Variant.ASL_AArch64 then if_asl_aarch64 else otherwise
 
     (**************************************************************************)
     (* Execution                                                              *)

herd/libdir/asl-pseudocode/patches-vmsa.asl

@@ -1,9 +1,9 @@
 // AArch64.S1Enabled()
 // ===================
 // Determine if stage 1 is enabled for the access type for this translation regime
-// Stage 1 is the onlt translation regime implemented
+// Stage 1 is the only translation regime implemented
 
-func AArch64_S1Enabled(regme : Regime,acctype : AccessType) => boolean
+func AArch64_S1Enabled(regime : Regime,acctype : AccessType) => boolean
 begin
   return TRUE;
 end
@@ -191,14 +191,25 @@ end
 // Perform HW update of table descriptor as an atomic operation
 // Modified -> disabled at the moment
 
-func AArch64_MemSwapTableDesc
+func No_AArch64_MemSwapTableDesc
   (fault_in:FaultRecord,prev_desc:bits(N),new_desc:bits(N),
   ee:bit,descaccess:AccessDescriptor,descpaddr:AddressDescriptor)
 => (FaultRecord, bits(N))
 begin
+  __debug__('1111');
   return (fault_in,new_desc);
 end
 
+func AArch64_MemSwapTableDesc
+  (fault_in:FaultRecord,prev_desc:bits(N),new_desc:bits(N),
+  ee:bit,descaccess:AccessDescriptor,descpaddr:AddressDescriptor)
+=> (FaultRecord, bits(N))
+begin
+   let addr = descpaddr.paddress.address;
+   WritePtePrimitive(addr,new_desc);
+   return (fault_in,new_desc);
+end
+
 // AArch64.DataAbort()
 // ===================
 
@@ -263,3 +274,42 @@ begin
 //  assert FALSE;
   return;
 end
+
+//
+// Previous walkparams
+// {aie:'0',amec:'0',cmow:'0',d128:'0',dc:'0',dct:'0',disch:'0',ds:'0',
+// e0pd:'0',ee:'0',emec:'0',epan:'0',fng:'0',ha:'0',haft:'0',hd:'0',
+// hpd:'0',irgn:'01',
+// mair:'0000000000000000000000000000000000000000000000000000000000000000',
+// mair2:'0000000000000000000000000000000000000000000000000000000000000000',
+// mtx:'0',nfd:'0',ntlsmd:'1',nv1:'0',orgn:'01',pie:'0',pir:'',pire0:'',
+// pnch:'0',ps:'100',sh:'11',sif:'0',skl:'00',t0sz:'000',t1sz:'000',
+// tbi:'0',tbid:'0',tgx:2,txsz:'010000',uwxn:'0',wxn:'0',}
+
+
+// AArch64.GetS1TTWParams()
+// ========================
+// Returns stage 1 translation table walk parameters from respective controlling
+// System registers.
+// Luc: we assume EL10 regime, return minimal parameters
+func AArch64_GetS1TTWParams
+  (regime:Regime, ss:SecurityState, va:bits(64))
+  => S1TTWParams
+begin
+  var walkparams : S1TTWParams;
+  assert (regime == Regime_EL10);
+  walkparams.ha = GetHaPrimitive();
+//  __debug__(walkparams);
+  return walkparams;
+end
+
+
+// AArch64.S1TxSZFaults()
+// ======================
+// Detect whether configuration of stage 1 TxSZ field generates a fault
+// Luc: Override: does not occur, never.
+
+func AArch64_S1TxSZFaults (regime:Regime,walkparams:S1TTWParams) => boolean
+begin
+  return FALSE;
+end

herd/libdir/asl-pseudocode/physmem-vmsa.asl

@@ -19,7 +19,7 @@ begin
   else
     eventaccess = PHY_PTE;
   end
-// No, we can write, physically.
+// Now, we can write, physically.
   write_memory_gen (desc.paddress.address, size*8, value,accdesc,eventaccess);
   return PhysMemRetStatus {
     statuscode = Fault_None,