diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 8fbe0660e4..f99d5f3efa 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -408,16 +408,18 @@ struct
   let threadspawn ctx lval f args fctx =
     ctx.local
 
-  let event ctx e aprx =
+  let event ctx e octx =
     let st = ctx.local in
     match e with
-    | Events.Lock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.lock (Analyses.ask_of_ctx aprx) aprx.global st addr
+    | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
+      Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr
     | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.unlock (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st addr
+      if addr = UnknownPtr then
+        M.info ~category:Unsound "Unknown mutex unlocked, apron privatization unsound"; (* TODO: something more sound *)
+      Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr
     (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *)
     | Events.EnterMultiThreaded ->
-      Priv.enter_multithreaded (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st
+      Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st
     | _ ->
       st
 
diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 0fe1b7b197..b2e0a64999 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -438,12 +438,17 @@ struct
     {st with apr = apr_local'}
 
   let lock ask getg (st: apron_components_t) m =
-    let apr = st.apr in
-    let get_m = get_m_with_mutex_inits ask getg m in
-    (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let get_m = keep_only_protected_globals ask m get_m in
-    let apr' = AD.meet apr get_m in
-    {st with apr = apr'}
+    (* TODO: somehow actually unneeded here? *)
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let apr = st.apr in
+      let get_m = get_m_with_mutex_inits ask getg m in
+      (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
+      let get_m = keep_only_protected_globals ask m get_m in
+      let apr' = AD.meet apr get_m in
+      {st with apr = apr'}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: apron_components_t) m: apron_components_t =
     let apr = st.apr in
@@ -942,15 +947,19 @@ struct
     {apr = apr_local'; priv = (W.add g w,LMust.add lm lmust,l')}
 
   let lock ask getg (st: apron_components_t) m =
-    let apr = st.apr in
-    let _,lmust,l = st.priv in
-    let lm = LLock.mutex m in
-    let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
-    let local_m = BatOption.default (LAD.bot ()) (L.find_opt lm l) in
-    (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let local_m = Cluster.keep_only_protected_globals ask m local_m in
-    let apr = Cluster.lock apr local_m get_m in
-    {st with apr}
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let apr = st.apr in
+      let _,lmust,l = st.priv in
+      let lm = LLock.mutex m in
+      let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
+      let local_m = BatOption.default (LAD.bot ()) (L.find_opt lm l) in
+      (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
+      let local_m = Cluster.keep_only_protected_globals ask m local_m in
+      let apr = Cluster.lock apr local_m get_m in
+      {st with apr}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: apron_components_t) m: apron_components_t =
     let apr = st.apr in
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2e846da692..1aa137c76e 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2367,15 +2367,17 @@ struct
   let event ctx e octx =
     let st: store = ctx.local in
     match e with
-    | Events.Lock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
+    | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
       if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr;
-      Priv.lock (Analyses.ask_of_ctx octx) (priv_getg octx.global) st addr
+      Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr
     | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.unlock (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st addr
+      if addr = UnknownPtr then
+        M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *)
+      Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
     | Events.Escape escaped ->
-      Priv.escape (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st escaped
+      Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped
     | Events.EnterMultiThreaded ->
-      Priv.enter_multithreaded (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st
+      Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
     | Events.AssignSpawnedThread (lval, tid) ->
       (* TODO: is this type right? *)
       set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 7d8d7179f2..da6c7b121b 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -276,18 +276,23 @@ struct
     cpa' *)
 
   let lock ask getg (st: BaseComponents (D).t) m =
-    let get_m = get_m_with_mutex_inits ask getg m in
-    (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
-       where our (necessary) original context still has the mutex,
-       so the query would be on the wrong lockset.
-       TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
-       Therefore, just use _without to exclude the mutex we shouldn't have.
-       In non-cond locks we don't have it anyway, so there's no difference.
-       No other privatization uses is_unprotected, so this hack is only needed here. *)
-    let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
-    let cpa' = CPA.filter is_in_V get_m in
-    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a\n" LockDomain.Addr.pretty m CPA.pretty cpa';
-    {st with cpa = CPA.fold CPA.add cpa' st.cpa}
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let get_m = get_m_with_mutex_inits ask getg m in
+      (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
+        where our (necessary) original context still has the mutex,
+        so the query would be on the wrong lockset.
+        TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
+        Therefore, just use _without to exclude the mutex we shouldn't have.
+        In non-cond locks we don't have it anyway, so there's no difference.
+        No other privatization uses is_unprotected, so this hack is only needed here. *)
+      let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
+      let cpa' = CPA.filter is_in_V get_m in
+      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a\n" LockDomain.Addr.pretty m CPA.pretty cpa';
+      {st with cpa = CPA.fold CPA.add cpa' st.cpa}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
+
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     let side_m_cpa = CPA.filter is_in_Gm st.cpa in
@@ -351,15 +356,20 @@ struct
     ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" d_varinfo x VD.pretty v CPA.pretty cpa');
     cpa' *)
 
-  let lock ask getg (st: BaseComponents (D).t) m =
-    let get_m = get_m_with_mutex_inits ask getg m in
-    (* Additionally filter get_m in case it contains variables it no longer protects. *)
-    let is_in_Gm x _ = is_protected_by ask m x in
-    let get_m = CPA.filter is_in_Gm get_m in
-    let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
-    let meet = long_meet st.cpa get_m in
-    if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a\n" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet;
-    {st with cpa = meet}
+  let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let get_m = get_m_with_mutex_inits ask getg m in
+      (* Additionally filter get_m in case it contains variables it no longer protects. *)
+      let is_in_Gm x _ = is_protected_by ask m x in
+      let get_m = CPA.filter is_in_Gm get_m in
+      let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
+      let meet = long_meet st.cpa get_m in
+      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a\n" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet;
+      {st with cpa = meet}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
+
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     sideg (V.mutex m) (CPA.filter is_in_Gm st.cpa);
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 98e140f86c..a12ed5a0fd 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -127,7 +127,7 @@ struct
     if !GU.global_initialization then
       Lockset.empty ()
     else
-      let ls = ask.f Queries.CurrentLockset in
+      let ls = ask.f Queries.MustLockset in
       Q.LS.fold (fun (var, offs) acc ->
           Lockset.add (Lock.from_var_offset (var, conv_offset offs)) acc
         ) ls (Lockset.empty ())
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 575aa14a55..75a8f98562 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -4,55 +4,52 @@ open Prelude.Ana
 open Analyses
 open DeadlockDomain
 
+
 module Spec =
 struct
-  include Analyses.IdentitySpec
-
-  let name () = "deadlock"
-
-  module D = MayLockEvents
-  module C = D
-  module V = Lock
 
   module LockEventPair = Printable.Prod (LockEvent) (LockEvent)
   module MayLockEventPairs = SetDomain.Make (LockEventPair)
-  module G =
-  struct
-    include MapDomain.MapBot (Lock) (MayLockEventPairs)
-    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
-  end
 
-  let side_lock_event_pair ctx before after =
-    let d =
-      if !GU.should_warn then
-        G.singleton (Tuple3.first after) (MayLockEventPairs.singleton (before, after))
-      else
-        G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
-    in
-    ctx.sideg (Tuple3.first before) d
+  module Arg =
+  struct
+    module D = MayLockEvents
+    module V = Lock
 
+    module G =
+    struct
+      include MapDomain.MapBot (Lock) (MayLockEventPairs)
+      let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
+    end
 
-  (* Some required states *)
-  let startstate _ : D.t = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
-  let exitstate  _ : D.t = D.empty ()
+    let side_lock_event_pair ctx before after =
+      let d =
+        if !GU.should_warn then
+          G.singleton (Tuple3.first after) (MayLockEventPairs.singleton (before, after))
+        else
+          G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
+      in
+      ctx.sideg (Tuple3.first before) d
 
-  let part_access ctx: MCPAccess.A.t =
-    Obj.obj (ctx.ask (PartAccess Point))
+    let part_access ctx: MCPAccess.A.t =
+      Obj.obj (ctx.ask (PartAccess Point))
 
-  let event ctx (e: Events.t) octx =
-    match e with
-    | Lock addr ->
-      let after = (addr, ctx.prev_node, part_access octx) in (* use octx for access to use locksets before event *)
+    let add ctx ((l, _): LockDomain.Lockset.Lock.t) =
+      let after: LockEvent.t = (l, ctx.prev_node, part_access ctx) in (* use octx for access to use locksets before event *)
       D.iter (fun before ->
           side_lock_event_pair ctx before after
         ) ctx.local;
       D.add after ctx.local
-    | Unlock addr ->
-      let inLockAddrs (e, _, _) = Lock.equal addr e in
+
+    let remove ctx l =
+      let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
-    | _ ->
-      ctx.local
+  end
+
+  include LocksetAnalysis.MakeMay (Arg)
+  let name () = "deadlock"
+
+  module G = Arg.G (* help type checker using explicit constraint *)
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
@@ -64,15 +61,22 @@ struct
       (* TODO: find all cycles/SCCs *)
       let global_visited_locks = LH.create 100 in
 
+      let may_equal l1 l2 = match l1, l2 with
+        | ValueDomain.Addr.UnknownPtr, _
+        | _, ValueDomain.Addr.UnknownPtr ->
+          true
+        | _, _ -> Lock.equal l1 l2
+      in
+
       (* DFS *)
       let rec iter_lock (path_visited_locks: LS.t) (path_visited_lock_event_pairs: LockEventPair.t list) (lock: Lock.t) =
-        if LS.mem lock path_visited_locks then (
+        if LS.mem lock path_visited_locks || LS.mem ValueDomain.Addr.UnknownPtr path_visited_locks || (not (LS.is_empty path_visited_locks) && lock = ValueDomain.Addr.UnknownPtr) then (
           (* cycle may not return to first lock, but an intermediate one, cut off the non-cyclic stem *)
           let path_visited_lock_event_pairs =
             (* path_visited_lock_event_pairs cannot be empty *)
             List.hd path_visited_lock_event_pairs ::
             List.take_while (fun (_, (after_lock, _, _)) ->
-                not (Lock.equal after_lock lock)
+                not (may_equal after_lock lock)
               ) (List.tl path_visited_lock_event_pairs)
           in
           let mhp =
@@ -114,4 +118,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis ~dep:["mutex"] (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec)
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
new file mode 100644
index 0000000000..47167282eb
--- /dev/null
+++ b/src/analyses/locksetAnalysis.ml
@@ -0,0 +1,88 @@
+(** Basic lockset analyses. *)
+
+open Prelude.Ana
+open Analyses
+
+
+module type DS =
+sig
+  include Lattice.S
+  val empty: unit -> t
+end
+
+module Make (D: DS) =
+struct
+  include Analyses.IdentitySpec
+  let name () = "lockset"
+
+  module D = D
+  module C = D
+
+  let startstate v = D.empty ()
+  let threadenter ctx lval f args = [D.empty ()]
+  let exitstate  v = D.empty ()
+end
+
+
+module type MayArg =
+sig
+  module D: DS
+  module G: Lattice.S
+  module V: Printable.S
+
+  val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
+  val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
+end
+
+module MakeMay (Arg: MayArg) =
+struct
+  include Make (Arg.D)
+  let name () = "mayLockset"
+
+  module G = Arg.G
+  module V = Arg.V
+
+  let event ctx e octx =
+    match e with
+    | Events.Lock l ->
+      Arg.add ctx l (* add all locks, including blob and unknown *)
+    | Events.Unlock UnknownPtr ->
+      ctx.local (* don't remove any locks, including unknown itself *)
+    | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) ->
+      ctx.local (* don't remove non-unique lock *)
+    | Events.Unlock l ->
+      Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *)
+    | _ ->
+      ctx.local
+end
+
+
+module type MustArg =
+sig
+  include MayArg
+  val remove_all: (D.t, _, D.t, _) ctx -> D.t
+end
+
+module MakeMust (Arg: MustArg) =
+struct
+  include Make (Arg.D)
+  let name () = "mustLockset"
+
+  module G = Arg.G
+  module V = Arg.V
+
+  let event ctx e octx =
+    match e with
+    | Events.Lock (UnknownPtr, _) ->
+      ctx.local (* don't add unknown lock *)
+    | Events.Lock (Addr (v, _), _) when ctx.ask (IsMultiple v) ->
+      ctx.local (* don't add non-unique lock *)
+    | Events.Lock l ->
+      Arg.add ctx l (* add definite lock or none in parallel if ambiguous *)
+    | Events.Unlock UnknownPtr ->
+      Arg.remove_all ctx (* remove all locks *)
+    | Events.Unlock l ->
+      Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
+    | _ ->
+      ctx.local
+end
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index f7354b4d86..20cffa6afb 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -1,76 +1,28 @@
-(** May-lockset analysis. *)
+(** May lockset analysis (unused). *)
 
 open Prelude.Ana
 open Analyses
 
-module Spec =
+module Arg =
 struct
-  include Analyses.DefaultSpec
-
-  let name () = "maylocks"
   module D = LockDomain.MayLockset
-  module C = LockDomain.MayLockset
-
-  (* transfer functions : usual operation just propagates the value *)
-  let assign ctx (lval:lval) (rval:exp) : D.t = ctx.local
-  let branch ctx (exp:exp) (tv:bool) : D.t = ctx.local
-  let body ctx (f:fundec) : D.t = ctx.local
-  let return ctx (exp:exp option) (f:fundec) : D.t = ctx.local
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = [ctx.local,ctx.local]
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = au
-
-  (* Helper function to convert query-offsets to valuedomain-offsets *)
-  let rec conv_offset x =
-    match x with
-    | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
-    | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
-    | `Field (f,o) -> `Field (f, conv_offset o)
+  module G = DefaultSpec.G
+  module V = DefaultSpec.V
 
-  (* Query the value (of the locking argument) to a list of locks. *)
-  let eval_exp_addr (a: Queries.ask) exp =
-    let gather_addr (v,o) b = ValueDomain.Addr.from_var_offset (v,conv_offset o) :: b in
-    match a.f (Queries.MayPointTo exp) with
-    | a when not (Queries.LS.is_top a) ->
-      Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
-    | b -> Messages.warn "Could not evaluate '%a' to an points-to set, instead got '%a'." d_exp exp Queries.LS.pretty b; []
+  let add ctx l =
+    D.add l ctx.local
 
-  (* locking logic -- add all locks we can add *)
-  let lock ctx rw may_fail return_value_on_success a lv arglist ls : D.ReverseAddrSet.t =
-    let add_one ls e = D.add (e,rw) ls in
-    let nls = List.fold_left add_one ls (List.concat_map (eval_exp_addr a) arglist) in
-    match lv with
-    | None -> nls
-    | Some lv ->
-      ctx.split nls [Events.SplitBranch (Lval lv, return_value_on_success)];
-      if may_fail then ctx.split ls [Events.SplitBranch (Lval lv, not return_value_on_success)];
-      raise Analyses.Deadcode
-
-  (* transfer function to handle library functions --- for us locking & unlocking *)
-  let special ctx (lv: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    let remove_rw x st = D.remove (x,true) (D.remove (x,false) st) in
-    (* unlocking logic *)
-    let unlock remove_fn =
-      match arglist with
-      | x::xs -> begin match  (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with
-          | [x] -> remove_fn x ctx.local
-          | _ -> ctx.local
-        end
-      | _ -> ctx.local
-    in
-    match (LibraryFunctions.classify f.vname arglist, f.vname) with
-    | `Lock (failing, rw, return_value_on_success), _
-      -> lock ctx rw failing return_value_on_success (Analyses.ask_of_ctx ctx) lv arglist ctx.local
-    | `Unlock, _
-      -> unlock remove_rw
+  let remove ctx l =
+    D.remove (l, true) (D.remove (l, false) ctx.local)
+end
 
-    | _ -> ctx.local
+module Spec =
+struct
+  include LocksetAnalysis.MakeMay (Arg)
+  let name () = "maylocks"
 
-  let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
-  let exitstate  v = D.top ()
+  let exitstate  v = D.top () (* TODO: why? *)
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec)
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index e2cf12540e..18459b4d7e 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -1,4 +1,4 @@
-(** Mutex analysis. *)
+(** Protecting mutex analysis. Must locksets locally and for globals. *)
 
 module M = Messages
 module Addr = ValueDomain.Addr
@@ -9,9 +9,6 @@ open Prelude.Ana
 open Analyses
 open GobConfig
 
-let big_kernel_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType))
-let console_sem = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType))
-let verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType))
 
 module type SpecParam =
 sig
@@ -20,94 +17,47 @@ sig
   val check_fun: ?write:bool -> Lockset.t -> G.t
 end
 
-(** Mutex analyzer without base --- this is the new standard *)
 module MakeSpec (P: SpecParam) =
 struct
-  include Analyses.DefaultSpec
-
-  (** name for the analysis (btw, it's "Only Mutex Must") *)
+  module Arg =
+  struct
+    module D = Lockset
+    module G = P.G
+    module V = VarinfoV
+
+    let add ctx l =
+      D.add l ctx.local
+
+    let remove ctx l =
+      D.remove (l, true) (D.remove (l, false) ctx.local)
+
+    let remove_all ctx =
+      (* Mutexes.iter (fun m ->
+          ctx.emit (MustUnlock m)
+        ) (D.export_locks ctx.local); *)
+      (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *)
+      D.empty ()
+  end
+  include LocksetAnalysis.MakeMust (Arg)
   let name () = "mutex"
 
-  (** Add current lockset alongside to the base analysis domain. Global data is collected using dirty side-effecting. *)
-  module D = Lockset
-  module C = Lockset
+  module D = Arg.D (* help type checker using explicit constraint *)
+  let should_join x y = D.equal x y
 
-  (** We do not add global state, so just lift from [BS]*)
+  (** Global data is collected using dirty side-effecting. *)
   module G = P.G
   module V = VarinfoV
 
-  let should_join x y = D.equal x y
-
-  (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain
-     element) answers with the string "unknown" on all non-concrete cases. *)
-  let rec conv_offset x =
-    match x with
-    | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
-    | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
-    | `Field (f,o) -> `Field (f, conv_offset o)
-
   let rec conv_offset_inv = function
     | `NoOffset -> `NoOffset
     | `Field (f, o) -> `Field (f, conv_offset_inv o)
-    (* TODO: better indices handling *)
-    | `Index (_, o) -> `Index (MyCFG.unknown_exp, conv_offset_inv o)
-
-
-  let eval_exp_addr (a: Queries.ask) exp =
-    let gather_addr (v,o) b = ValueDomain.Addr.from_var_offset (v,conv_offset o) :: b in
-    match a.f (Queries.MayPointTo exp) with
-    | a when not (Queries.LS.is_top a)
-                   && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) a) ->
-      Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
-    | _ -> []
-
-  let lock ctx rw may_fail nonzero_return_when_aquired a lv arglist ls =
-    let is_a_blob addr =
-      match LockDomain.Addr.to_var addr with
-      | Some a -> a.vname.[0] = '('
-      | None -> false
-    in
-    let lock_one (e:LockDomain.Addr.t) =
-      if is_a_blob e then
-        ls
-      else begin
-        let nls = Lockset.add (e,rw) ls in
-        let changed = Lockset.compare ls nls <> 0 in
-        match lv with
-        | None ->
-          if may_fail then
-            ls
-          else (
-            (* If the lockset did not change, do not emit Lock event *)
-            if changed then ctx.emit (Events.Lock e);
-            nls
-          )
-        | Some lv ->
-          let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in
-          if changed then
-            ctx.split nls [sb; Events.Lock e]
-          else
-            ctx.split nls [sb];
-          if may_fail then (
-            let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in
-            ctx.split ls [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)]
-          );
-          raise Analyses.Deadcode
-      end
-    in
-    match arglist with
-    | [x] -> begin match  (eval_exp_addr a x) with
-        | [e]  -> lock_one e
-        | _ -> ls
-      end
-    | _ -> Lockset.top ()
-
-
-  (** We just lift start state, global and dependency functions: *)
-  let startstate v = Lockset.empty ()
-  let threadenter ctx lval f args = [Lockset.empty ()]
-  let exitstate  v = Lockset.empty ()
+    | `Index (i, o) ->
+      let i_exp =
+        match ValueDomain.IndexDomain.to_int i with
+        | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
+        | None -> MyCFG.unknown_exp
+      in
+      `Index (i_exp, conv_offset_inv o)
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     let non_overlapping locks1 locks2 =
@@ -139,7 +89,7 @@ struct
         true
       else *)
         G.leq (ctx.global global) held_locks
-    | Queries.CurrentLockset ->
+    | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
       let ls = Mutexes.fold (fun addr ls ->
           match Addr.to_var_offset addr with
@@ -150,7 +100,7 @@ struct
       ls
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
-      Mutexes.mem verifier_atomic held_locks
+      Mutexes.mem MutexEventsAnalysis.verifier_atomic held_locks
     | _ -> Queries.Result.top q
 
   module A =
@@ -172,121 +122,6 @@ struct
       (* when reading: bump reader locks to exclusive as they protect reads *)
       Lockset.map (fun (x,_) -> (x,true)) ctx.local
 
-  (** Transfer functions: *)
-
-  let assign ctx lval rval : D.t =
-    ctx.local
-
-  let branch ctx exp tv : D.t =
-    ctx.local
-
-  let return ctx exp fundec : D.t =
-    (* deprecated but still valid SV-COMP convention for atomic block *)
-    if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then (
-      ctx.emit (Events.Unlock verifier_atomic);
-      Lockset.remove (verifier_atomic, true) ctx.local
-    )
-    else
-      ctx.local
-
-  let body ctx f : D.t =
-    (* deprecated but still valid SV-COMP convention for atomic block *)
-    if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then (
-      ctx.emit (Events.Lock verifier_atomic);
-      Lockset.add (verifier_atomic, true) ctx.local
-    )
-    else
-      ctx.local
-
-  let special ctx lv f arglist : D.t =
-    let remove_rw x st =
-      ctx.emit (Events.Unlock x);
-      Lockset.remove (x,true) (Lockset.remove (x,false) st)
-    in
-    let unlock remove_fn =
-      let remove_nonspecial x =
-        if Lockset.is_top x then x else
-          Lockset.filter (fun (v,_) -> match LockDomain.Addr.to_var v with
-              | Some v when v.vname.[0] = '{' -> true
-              | _ -> false
-            ) x
-      in
-      match arglist with
-      | x::xs -> begin match  (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with
-          | [] -> remove_nonspecial ctx.local
-          | es -> List.fold_right remove_fn es ctx.local
-        end
-      | _ -> ctx.local
-    in
-    match (LF.classify f.vname arglist, f.vname) with
-    | _, "_lock_kernel" ->
-      ctx.emit (Events.Lock big_kernel_lock);
-      Lockset.add (big_kernel_lock,true) ctx.local
-    | _, "_unlock_kernel" ->
-      ctx.emit (Events.Unlock big_kernel_lock);
-      Lockset.remove (big_kernel_lock,true) ctx.local
-    | `Lock (failing, rw, nonzero_return_when_aquired), _
-      -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in
-      (*print_endline @@ "Mutex `Lock "^f.vname;*)
-      lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arglist ctx.local
-    | `Unlock, "__raw_read_unlock"
-    | `Unlock, "__raw_write_unlock"  ->
-      let drop_raw_lock x =
-        let rec drop_offs o =
-          match o with
-          | `Field ({fname="raw_lock"; _},`NoOffset) -> `NoOffset
-          | `Field (f1,o1) -> `Field (f1, drop_offs o1)
-          | `Index (i1,o1) -> `Index (i1, drop_offs o1)
-          | `NoOffset -> `NoOffset
-        in
-        match Addr.to_var_offset x with
-        | Some (v,o) -> Addr.from_var_offset (v, drop_offs o)
-        | None -> x
-      in
-      unlock (fun l -> remove_rw (drop_raw_lock l))
-    | `Unlock, _ ->
-      (*print_endline @@ "Mutex `Unlock "^f.vname;*)
-      unlock remove_rw
-    | _, "spinlock_check" -> ctx.local
-    | _, "acquire_console_sem" when get_bool "kernel" ->
-      ctx.emit (Events.Lock console_sem);
-      Lockset.add (console_sem,true) ctx.local
-    | _, "release_console_sem" when get_bool "kernel" ->
-      ctx.emit (Events.Unlock console_sem);
-      Lockset.remove (console_sem,true) ctx.local
-    | _, "__builtin_prefetch" | _, "misc_deregister" ->
-      ctx.local
-    | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" ->
-      ctx.emit (Events.Lock verifier_atomic);
-      Lockset.add (verifier_atomic, true) ctx.local
-    | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" ->
-      ctx.emit (Events.Unlock verifier_atomic);
-      Lockset.remove (verifier_atomic, true) ctx.local
-    | _, "pthread_cond_wait"
-    | _, "pthread_cond_timedwait" ->
-      (* mutex is unlocked while waiting but relocked when returns *)
-      (* emit unlock-lock events for privatization *)
-      let m_arg = List.nth arglist 1 in
-      let ms = eval_exp_addr (Analyses.ask_of_ctx ctx) m_arg in
-      List.iter (fun m ->
-          (* unlock-lock each possible mutex as a split to be dependent *)
-          (* otherwise may-point-to {a, b} might unlock a, but relock b *)
-          ctx.split ctx.local [Events.Unlock m; Events.Lock m];
-        ) ms;
-      raise Deadcode (* splits cover all cases *)
-    | _, x ->
-      ctx.local
-
-  let enter ctx lv f args : (D.t * D.t) list =
-    [(ctx.local,ctx.local)]
-
-  let combine ctx lv fexp f args fc al =
-    al
-
-
-  let threadspawn ctx lval f args fctx =
-    ctx.local
-
   let event ctx e octx =
     match e with
     | Events.Access {var_opt; write} ->
@@ -301,8 +136,7 @@ struct
       end;
       ctx.local
     | _ ->
-      ctx.local
-
+      event ctx e octx (* delegate to must lockset analysis *)
 end
 
 module MyParam =
@@ -336,4 +170,4 @@ end
 module Spec = MakeSpec (WriteBased)
 
 let _ =
-  MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutexEvents"; "access"] (module Spec : MCPSpec)
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
new file mode 100644
index 0000000000..474ec3f63d
--- /dev/null
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -0,0 +1,145 @@
+(** Mutex events analysis (Lock and Unlock). *)
+
+module M = Messages
+module Addr = ValueDomain.Addr
+module Lockset = LockDomain.Lockset
+module Mutexes = LockDomain.Mutexes
+module LF = LibraryFunctions
+open Prelude.Ana
+open Analyses
+open GobConfig
+
+let big_kernel_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType))
+let console_sem = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType))
+let verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType))
+
+module Spec: MCPSpec =
+struct
+  include UnitAnalysis.Spec
+  let name () = "mutexEvents"
+
+
+  (* Currently we care only about concrete indexes. *)
+  let rec conv_offset x =
+    match x with
+    | `NoOffset    -> `NoOffset
+    | `Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
+    | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
+    | `Field (f,o) -> `Field (f, conv_offset o)
+
+  let eval_exp_addr (a: Queries.ask) exp =
+    let gather_addr (v,o) b = ValueDomain.Addr.from_var_offset (v,conv_offset o) :: b in
+    match a.f (Queries.MayPointTo exp) with
+    | a when Queries.LS.is_top a ->
+      [Addr.UnknownPtr]
+    | a ->
+      let top_elt = (dummyFunDec.svar, `NoOffset) in
+      let addrs = Queries.LS.fold gather_addr (Queries.LS.remove top_elt a) [] in
+      if Queries.LS.mem top_elt a then
+        Addr.UnknownPtr :: addrs
+      else
+        addrs
+
+  let lock ctx rw may_fail nonzero_return_when_aquired a lv arg =
+    match lv with
+    | None ->
+      List.iter (fun e ->
+          ctx.split () [Events.Lock (e, rw)]
+        ) (eval_exp_addr a arg);
+      if may_fail then
+        ctx.split () [];
+      raise Analyses.Deadcode
+    | Some lv ->
+      let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in
+      List.iter (fun e ->
+          ctx.split () [sb; Events.Lock (e, rw)];
+        ) (eval_exp_addr a arg);
+      if may_fail then (
+        let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in
+        ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)]
+      );
+      raise Analyses.Deadcode
+
+
+
+  let return ctx exp fundec : D.t =
+    (* deprecated but still valid SV-COMP convention for atomic block *)
+    if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then
+      ctx.emit (Events.Unlock verifier_atomic)
+
+  let body ctx f : D.t =
+    (* deprecated but still valid SV-COMP convention for atomic block *)
+    if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then
+      ctx.emit (Events.Lock (verifier_atomic, true))
+
+  let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t =
+    let remove_rw x = x in
+    let unlock remove_fn =
+      match arglist with
+      | [arg] ->
+        List.iter (fun e ->
+            ctx.split () [Events.Unlock (remove_fn e)]
+          ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg);
+        raise Analyses.Deadcode
+      | _ -> failwith "unlock has multiple arguments"
+    in
+    match (LF.classify f.vname arglist, f.vname) with
+    | _, "_lock_kernel" ->
+      ctx.emit (Events.Lock (big_kernel_lock, true))
+    | _, "_unlock_kernel" ->
+      ctx.emit (Events.Unlock big_kernel_lock)
+    | `Lock (failing, rw, nonzero_return_when_aquired), _ ->
+      begin match arglist with
+        | [arg] ->
+          (*print_endline @@ "Mutex `Lock "^f.vname;*)
+          lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arg
+        | _ -> failwith "lock has multiple arguments"
+      end
+    | `Unlock, "__raw_read_unlock"
+    | `Unlock, "__raw_write_unlock"  ->
+      let drop_raw_lock x =
+        let rec drop_offs o =
+          match o with
+          | `Field ({fname="raw_lock"; _},`NoOffset) -> `NoOffset
+          | `Field (f1,o1) -> `Field (f1, drop_offs o1)
+          | `Index (i1,o1) -> `Index (i1, drop_offs o1)
+          | `NoOffset -> `NoOffset
+        in
+        match Addr.to_var_offset x with
+        | Some (v,o) -> Addr.from_var_offset (v, drop_offs o)
+        | None -> x
+      in
+      unlock (fun l -> remove_rw (drop_raw_lock l))
+    | `Unlock, _ ->
+      (*print_endline @@ "Mutex `Unlock "^f.vname;*)
+      unlock remove_rw
+    | _, "spinlock_check" -> ()
+    | _, "acquire_console_sem" when get_bool "kernel" ->
+      ctx.emit (Events.Lock (console_sem, true))
+    | _, "release_console_sem" when get_bool "kernel" ->
+      ctx.emit (Events.Unlock console_sem)
+    | _, "__builtin_prefetch" | _, "misc_deregister" ->
+      ()
+    | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" ->
+      ctx.emit (Events.Lock (verifier_atomic, true))
+    | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" ->
+      ctx.emit (Events.Unlock verifier_atomic)
+    | _, "pthread_cond_wait"
+    | _, "pthread_cond_timedwait" ->
+      (* mutex is unlocked while waiting but relocked when returns *)
+      (* emit unlock-lock events for privatization *)
+      let m_arg = List.nth arglist 1 in
+      let ms = eval_exp_addr (Analyses.ask_of_ctx ctx) m_arg in
+      List.iter (fun m ->
+          (* unlock-lock each possible mutex as a split to be dependent *)
+          (* otherwise may-point-to {a, b} might unlock a, but relock b *)
+          ctx.split () [Events.Unlock m; Events.Lock (m, true)];
+        ) ms;
+      raise Deadcode (* splits cover all cases *)
+    | _, x ->
+      ()
+
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml
index dd62f1a898..05a26f3975 100644
--- a/src/analyses/osek.ml
+++ b/src/analyses/osek.ml
@@ -248,7 +248,26 @@ struct
     let check_fun = effect_fun
   end
 
-  module M = Mutex.MakeSpec (MyParam)
+  module M =
+  struct
+    include Mutex.MakeSpec (MyParam)
+
+    let extract_lock lock =
+      match lock with
+      | AddrOf (Var varinfo,NoOffset) -> LockDomain.Addr.from_var varinfo
+      | _ -> assert false
+
+    let special ctx lval f args =
+      (* simulate old mutex analysis special by emitting events directly, a la mutexEvents *)
+      begin match f.vname, args with
+        | ("GetResource" | "GetSpinlock"), [lock] ->
+          ctx.emit (Events.Lock (extract_lock lock, true))
+        | ("ReleaseResource" | "ReleaseSpinlock"), [lock] ->
+          ctx.emit (Events.Unlock (extract_lock lock))
+        | _, _ -> ()
+      end;
+      special ctx lval f args
+  end
   module Offs = ValueDomain.Offs
   module Lockset = LockDomain.Lockset
 
@@ -567,7 +586,7 @@ struct
           (*             offpry_flags flagstate v *)
           (*           end *)
         in off > pry
-    | Queries.CurrentLockset -> (* delegate for MinePriv *)
+    | Queries.MustLockset -> (* delegate for MinePriv *)
       (* TODO: delegate other queries? *)
       M.query ctx q
     | _ -> Queries.Result.top q
@@ -863,6 +882,8 @@ struct
     | _ -> M.special ctx lval f arglist
   (* with | _ -> M.special ctx lval f arglist (* suppress all fails  *) *)
 
+  let event ctx e = M.event ctx e
+
   let name () = "OSEK"
   let es_to_string f _ = f.svar.vname
 
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 5d1cf1825f..30223b7c61 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -3,7 +3,7 @@
 open Prelude.Ana
 open Analyses
 
-module Spec : Analyses.MCPSpec =
+module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Lattice.Unit =
 struct
   include Analyses.DefaultSpec
 
diff --git a/src/domains/events.ml b/src/domains/events.ml
index e62ac8bef9..7629da173d 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -1,7 +1,7 @@
 open Prelude.Ana
 
 type t =
-  | Lock of LockDomain.Addr.t  (** This is only emitted if the mutex was not previously held *)
+  | Lock of LockDomain.Lockset.Lock.t
   | Unlock of LockDomain.Addr.t
   | Escape of EscapeDomain.EscapedVars.t
   | EnterMultiThreaded
@@ -11,8 +11,8 @@ type t =
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *)
 
 let pretty () = function
-  | Lock m -> dprintf "Lock %a" LockDomain.Addr.pretty m
-  | Unlock m -> dprintf "Unock %a" LockDomain.Addr.pretty m
+  | Lock m -> dprintf "Lock %a" LockDomain.Lockset.Lock.pretty m
+  | Unlock m -> dprintf "Unlock %a" LockDomain.Addr.pretty m
   | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped
   | EnterMultiThreaded -> text "EnterMultiThreaded"
   | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 79cdefe96c..b67fa98699 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -77,7 +77,7 @@ type _ t =
   | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *)
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
-  | CurrentLockset: LS.t t
+  | MustLockset: LS.t t
   | MustBeAtomic: MustBool.t t
   | MustBeSingleThreaded: MustBool.t t
   | MustBeUniqueThread: MustBool.t t
@@ -124,7 +124,7 @@ struct
     | MayPointTo _ -> (module LS)
     | ReachableFrom _ -> (module LS)
     | Regions _ -> (module LS)
-    | CurrentLockset -> (module LS)
+    | MustLockset -> (module LS)
     | EvalFunvar _ -> (module LS)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
@@ -175,7 +175,7 @@ struct
     | MayPointTo _ -> LS.top ()
     | ReachableFrom _ -> LS.top ()
     | Regions _ -> LS.top ()
-    | CurrentLockset -> LS.top ()
+    | MustLockset -> LS.top ()
     | EvalFunvar _ -> LS.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
@@ -228,7 +228,7 @@ struct
     | Any (MayBePublic _) -> 7
     | Any (MayBePublicWithout _) -> 8
     | Any (MustBeProtectedBy _) -> 9
-    | Any CurrentLockset -> 10
+    | Any MustLockset -> 10
     | Any MustBeAtomic -> 11
     | Any MustBeSingleThreaded -> 12
     | Any MustBeUniqueThread -> 13
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 4edff233e0..63d2dda10d 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -291,7 +291,7 @@
           "items": { "type": "string" },
           "default": [
             "expRelation", "base", "threadid", "threadflag", "threadreturn",
-            "escape", "mutex", "access", "mallocWrapper", "mhp"
+            "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp"
           ]
         },
         "path_sens": {
diff --git a/tests/regression/02-base/06-side_effect1.c b/tests/regression/02-base/06-side_effect1.c
index 5805ad90a5..12f9339dbd 100644
--- a/tests/regression/02-base/06-side_effect1.c
+++ b/tests/regression/02-base/06-side_effect1.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 
 #include<pthread.h>
 #include<assert.h>
diff --git a/tests/regression/02-base/07-side_effect2.c b/tests/regression/02-base/07-side_effect2.c
index 54fa953a9d..eeb8af62b5 100644
--- a/tests/regression/02-base/07-side_effect2.c
+++ b/tests/regression/02-base/07-side_effect2.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 
 #include<pthread.h>
 #include<assert.h>
diff --git a/tests/regression/02-base/09-ambigpointer.c b/tests/regression/02-base/09-ambigpointer.c
index 085f44b7e7..c23d9a00f8 100644
--- a/tests/regression/02-base/09-ambigpointer.c
+++ b/tests/regression/02-base/09-ambigpointer.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 #include<pthread.h>
 #include<assert.h>
 
diff --git a/tests/regression/02-base/10-init_allfuns.c b/tests/regression/02-base/10-init_allfuns.c
index 22c84810a1..1f2a5de0df 100644
--- a/tests/regression/02-base/10-init_allfuns.c
+++ b/tests/regression/02-base/10-init_allfuns.c
@@ -1,4 +1,4 @@
-// PARAM: --enable allfuns --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --enable allfuns --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 int glob1 = 5;
 int glob2 = 7;
 
diff --git a/tests/regression/02-base/23-malloc_globmt.c b/tests/regression/02-base/23-malloc_globmt.c
index 2d008596af..66b8eb0047 100644
--- a/tests/regression/02-base/23-malloc_globmt.c
+++ b/tests/regression/02-base/23-malloc_globmt.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 #include <stdlib.h>
 #include <pthread.h>
 #include <assert.h>
diff --git a/tests/regression/02-base/30-escape_sound.c b/tests/regression/02-base/30-escape_sound.c
index cbafdd2678..1e72a4d044 100644
--- a/tests/regression/02-base/30-escape_sound.c
+++ b/tests/regression/02-base/30-escape_sound.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 
 #include<pthread.h>
 #include<stdio.h>
diff --git a/tests/regression/02-base/41-calloc_globmt.c b/tests/regression/02-base/41-calloc_globmt.c
index 50ddba8622..7445dc1b85 100644
--- a/tests/regression/02-base/41-calloc_globmt.c
+++ b/tests/regression/02-base/41-calloc_globmt.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" --set ana.int.interval true --set ana.base.arrays.domain partitioned
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" --set ana.int.interval true --set ana.base.arrays.domain partitioned
 #include <stdlib.h>
 #include <pthread.h>
 #include <assert.h>
diff --git a/tests/regression/03-practical/14-call_by_pointer.c b/tests/regression/03-practical/14-call_by_pointer.c
index 9c1edd5248..b409c3dad3 100644
--- a/tests/regression/03-practical/14-call_by_pointer.c
+++ b/tests/regression/03-practical/14-call_by_pointer.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
+// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']"
 #include <assert.h>
 
 /**
diff --git a/tests/regression/04-mutex/63-unknown_unlock_rc.c b/tests/regression/04-mutex/63-unknown_unlock_rc.c
new file mode 100644
index 0000000000..0b896f3c6a
--- /dev/null
+++ b/tests/regression/04-mutex/63-unknown_unlock_rc.c
@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  pthread_mutex_t *m; // unknown
+  pthread_mutex_unlock(m);
+  myglobal=myglobal+1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/19-fail_deadlock.c b/tests/regression/15-deadlock/19-fail_deadlock.c
new file mode 100644
index 0000000000..0d35f7a2b5
--- /dev/null
+++ b/tests/regression/15-deadlock/19-fail_deadlock.c
@@ -0,0 +1,38 @@
+// PARAM: --set ana.activated[+] deadlock --enable sem.lock.fail
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  pthread_mutex_lock(&mutex2); // DEADLOCK
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_mutex_lock(&mutex2); // DEADLOCK
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(&mutex2);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 10000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/20-ambig_deadlock.c b/tests/regression/15-deadlock/20-ambig_deadlock.c
new file mode 100644
index 0000000000..69e47a4d33
--- /dev/null
+++ b/tests/regression/15-deadlock/20-ambig_deadlock.c
@@ -0,0 +1,45 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.path_sens[-] mutex
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  pthread_mutex_lock(&mutex2); // DEADLOCK
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  int k = rand() % 2;
+  pthread_mutex_t *m;
+  if (k)
+    m = &mutex2;
+  else
+    m = &mutex3;
+  pthread_mutex_lock(m); // DEADLOCK
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(m);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/21-unknown_deadlock.c b/tests/regression/15-deadlock/21-unknown_deadlock.c
new file mode 100644
index 0000000000..c68c76b592
--- /dev/null
+++ b/tests/regression/15-deadlock/21-unknown_deadlock.c
@@ -0,0 +1,41 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1); // TODO DEADLOCK?
+  pthread_mutex_lock(&mutex2); // TODO DEADLOCK?
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  int k = rand() % 2;
+  pthread_mutex_t *m; // unknown
+  pthread_mutex_lock(m); // DEADLOCK
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(m);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c b/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c
new file mode 100644
index 0000000000..52009f9c14
--- /dev/null
+++ b/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c
@@ -0,0 +1,51 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.path_sens[-] mutex
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  pthread_mutex_lock(&mutex2); // DEADLOCK
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  int k = rand() % 2;
+  int l = rand() % 2;
+  pthread_mutex_t *m, *n;
+  if (k)
+    m = &mutex2;
+  else
+    m = &mutex3;
+  if (l)
+    n = &mutex2;
+  else
+    n = &mutex3;
+  pthread_mutex_lock(m); // DEADLOCK
+  pthread_mutex_unlock(n);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(m);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c b/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c
new file mode 100644
index 0000000000..be54b8693f
--- /dev/null
+++ b/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c
@@ -0,0 +1,42 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1); // TODO DEADLOCK?
+  pthread_mutex_lock(&mutex2); // TODO DEADLOCK?
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  int k = rand() % 2;
+  pthread_mutex_t *m, *n; // unknown
+  pthread_mutex_lock(m); // DEADLOCK
+  pthread_mutex_unlock(n);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(m);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c b/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c
new file mode 100644
index 0000000000..2a1aa9dd6f
--- /dev/null
+++ b/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c
@@ -0,0 +1,49 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t *p, *q;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(p); // DEADLOCK
+  pthread_mutex_lock(q); // DEADLOCK
+  g1 = g2 + 1;
+  pthread_mutex_unlock(q);
+  pthread_mutex_unlock(p);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_mutex_lock(p); // DEADLOCK
+  pthread_mutex_unlock(p);
+  pthread_mutex_lock(q); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(q);
+  pthread_mutex_unlock(p);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  pthread_mutex_t *a;
+
+  for (i=0; i < 10; i++){
+    a = malloc(sizeof(pthread_mutex_t));
+    pthread_mutex_init(a,0);
+    if (i==3)
+      p = a;
+    if (i==7)
+      q = a;
+  }
+
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/25-malloc_deadlock.c b/tests/regression/15-deadlock/25-malloc_deadlock.c
new file mode 100644
index 0000000000..535bbf607c
--- /dev/null
+++ b/tests/regression/15-deadlock/25-malloc_deadlock.c
@@ -0,0 +1,48 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t *p, *q;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(p); // DEADLOCK
+  pthread_mutex_lock(q); // DEADLOCK
+  g1 = g2 + 1;
+  pthread_mutex_unlock(q);
+  pthread_mutex_unlock(p);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_mutex_lock(p); // DEADLOCK
+  pthread_mutex_lock(q); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(q);
+  pthread_mutex_unlock(p);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  pthread_mutex_t *a;
+
+  for (i=0; i < 10; i++){
+    a = malloc(sizeof(pthread_mutex_t));
+    pthread_mutex_init(a,0);
+    if (i==3)
+      p = a;
+    if (i==7)
+      q = a;
+  }
+
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/26-unknown_deadlock2.c b/tests/regression/15-deadlock/26-unknown_deadlock2.c
new file mode 100644
index 0000000000..398ff4e95b
--- /dev/null
+++ b/tests/regression/15-deadlock/26-unknown_deadlock2.c
@@ -0,0 +1,41 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex2); // TODO DEADLOCK?
+  pthread_mutex_lock(&mutex1); // TODO DEADLOCK?
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(&mutex2);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  int k = rand() % 2;
+  pthread_mutex_t *m; // unknown
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  pthread_mutex_lock(m); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(m);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 1000000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/27-self_deadlock.c b/tests/regression/15-deadlock/27-self_deadlock.c
new file mode 100644
index 0000000000..04b34b4a03
--- /dev/null
+++ b/tests/regression/15-deadlock/27-self_deadlock.c
@@ -0,0 +1,38 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  pthread_mutex_lock(&mutex1); // DEADLOCK
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_mutex_lock(&mutex2); // DEADLOCK
+  pthread_mutex_lock(&mutex2); // DEADLOCK
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex2);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 10000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}