diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index c5717cc5e7..5b8b2d0563 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -153,6 +153,7 @@ def collect_warnings
                     when /\(conf\. \d+\)/            then "race"
                     when /lockset:/                  then "race" # osek races have their own legacy-like output
                     when /Deadlock/                  then "deadlock"
+                    when /lock (before|after):/      then "deadlock"
                     when /Assertion .* will fail/    then "fail"
                     when /Assertion .* will succeed/ then "success"
                     when /Assertion .* is unknown/   then "unknown"
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 7514b80b6c..fc178d43cb 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -48,7 +48,7 @@ struct
     let part_access ctx (e:exp) (vo:varinfo option) (w: bool): MCPAccess.A.t =
       ctx.emit (Access {var_opt=vo; write=w});
       (*partitions & locks*)
-      Obj.obj (ctx.ask (PartAccess {exp=e; var_opt=vo; write=w}))
+      Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; write=w})))
     in
     let add_access conf vo oo =
       let a = part_access ctx e vo w in
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 8ee2433aed..575aa14a55 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -4,110 +4,114 @@ open Prelude.Ana
 open Analyses
 open DeadlockDomain
 
-let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref []
-
 module Spec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "deadlock"
 
-  (* The domain for the analysis *)
-  module D = DeadlockDomain.Lockset (* MayLockset *)
-  module C = DeadlockDomain.Lockset
-
-  let addLockingInfo newLock lockList =
-    let add_comb a b =
-      if List.exists (fun (x,y) -> MyLock.equal x a && MyLock.equal y b) !forbiddenList then ()
-      else forbiddenList := (a,b)::!forbiddenList
+  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
-
-    (* Check forbidden list *)
-    if !Goblintutil.postsolving then begin
-      D.iter (fun e -> List.iter (fun (a,b) ->
-          if ((MyLock.equal a e) && (MyLock.equal b newLock)) then (
-            Messages.warn "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty e.addr ValueDomain.Addr.pretty newLock.addr CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc CilType.Location.pretty b.loc CilType.Location.pretty a.loc;
-            Messages.warn ~loc:a.loc "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty newLock.addr ValueDomain.Addr.pretty e.addr CilType.Location.pretty b.loc CilType.Location.pretty a.loc CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc;
-          )
-          else () ) !forbiddenList ) lockList;
-
-      (* Add forbidden order *)
-      D.iter (
-        fun lock ->
-          add_comb newLock lock;
-          let transAddList = List.find_all (fun (a,b) -> MyLock.equal a lock) !forbiddenList in
-          List.iter (fun (a,b) -> add_comb newLock b) transAddList
-      ) lockList
-    end
+    ctx.sideg (Tuple3.first before) d
 
 
   (* Some required states *)
   let startstate _ : D.t = D.empty ()
   let threadenter ctx lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  _ : D.t = D.empty ()
 
-  (* ======== Transfer functions ======== *)
-  (* Called for assignments, branches, ... *)
-
-  (* Assignment lval <- exp *)
-  let assign ctx (lval:lval) (rval:exp) : D.t =
-    ctx.local
-
-  (* Branch *)
-  let branch ctx (exp:exp) (tv:bool) : D.t =
-    ctx.local
-
-  (* Body of a function starts *)
-  let body ctx (f:fundec) : D.t =
-    ctx.local
-
-  (* Returns from a function *)
-  let return ctx (exp:exp option) (f:fundec) : D.t =
-    ctx.local
-
-  (* Calls/Enters a function *)
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [D.bot (),ctx.local]
-
-  (* Leaves a function *)
-  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)
-
-  (* 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; []
-
-  (* Called when calling a special/unknown function *)
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    if D.is_top ctx.local then ctx.local else
-      match LibraryFunctions.classify f.vname arglist with
-      | `Lock (_, _, _) ->
-        List.fold_left (fun d lockAddr ->
-          addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local;
-          D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local
-        ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist))
-      | `Unlock ->
-        let lockAddrs = eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist) in
-        if List.compare_length_with lockAddrs 1 = 0 then
-          let inLockAddrs e = List.exists (fun r -> ValueDomain.Addr.equal r e.addr) lockAddrs in
-          D.filter (neg inLockAddrs) ctx.local
-        else ctx.local
-      | _ -> ctx.local
-
+  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 *)
+      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
+      D.filter (neg inLockAddrs) ctx.local
+    | _ ->
+      ctx.local
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | WarnGlobal g ->
+      let g: V.t = Obj.obj g in
+
+      let module LH = Hashtbl.Make (Lock) in
+      let module LS = Set.Make (Lock) in
+      (* TODO: find all cycles/SCCs *)
+      let global_visited_locks = LH.create 100 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 (
+          (* 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)
+              ) (List.tl path_visited_lock_event_pairs)
+          in
+          let mhp =
+            Enum.cartesian_product (List.enum path_visited_lock_event_pairs) (List.enum path_visited_lock_event_pairs)
+            |> Enum.for_all (fun (((_, (_, _, access1)) as p1), ((_, (_, _, access2)) as p2)) ->
+                LockEventPair.equal p1 p2 || MCPAccess.A.may_race access1 access2
+              )
+          in
+          if mhp then (
+            (* normalize path_visited_lock_event_pairs such that we don't get the same cycle multiple times, starting from different events *)
+            let min = List.min ~cmp:LockEventPair.compare path_visited_lock_event_pairs in
+            let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in
+            let (init, tail) = List.split_at mini path_visited_lock_event_pairs in
+            let normalized = List.rev_append init (List.rev tail) in (* backwards to get correct printout order *)
+            let msgs = List.concat_map (fun ((before_lock, before_node, before_access), (after_lock, after_node, after_access)) ->
+                [
+                  (Pretty.dprintf "lock before: %a with %a" Lock.pretty before_lock MCPAccess.A.pretty before_access, Some (UpdateCil.getLoc before_node));
+                  (Pretty.dprintf "lock after: %a with %a" Lock.pretty after_lock MCPAccess.A.pretty after_access, Some (UpdateCil.getLoc after_node));
+                ]
+              ) normalized
+            in
+            M.msg_group Warning ~category:Deadlock "Locking order cycle" msgs
+          )
+        )
+        else if not (LH.mem global_visited_locks lock) then begin
+          LH.replace global_visited_locks lock ();
+          let new_path_visited_locks = LS.add lock path_visited_locks in
+          G.iter (fun to_lock lock_event_pairs ->
+              MayLockEventPairs.iter (fun lock_event_pair ->
+                  let new_path_visited_lock_event_pairs' = lock_event_pair :: path_visited_lock_event_pairs in
+                  iter_lock new_path_visited_locks new_path_visited_lock_event_pairs' to_lock
+                ) lock_event_pairs
+            ) (ctx.global lock)
+        end
+      in
+
+      Stats.time "deadlock" (iter_lock LS.empty []) g
+    | _ -> Queries.Result.top q
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutex"] (module Spec : MCPSpec)
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 8d5638be5b..b6f15a7dde 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -275,8 +275,8 @@ struct
           (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
           let (n, g): V.t = Obj.obj g in
           f ~q:(WarnGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
-        | Queries.PartAccess {exp; var_opt; write} ->
-          Obj.repr (access ctx exp var_opt write)
+        | Queries.PartAccess a ->
+          Obj.repr (access ctx a)
         (* | EvalInt e ->
            (* TODO: only query others that actually respond to EvalInt *)
            (* 2x speed difference on SV-COMP nla-digbench-scaling/ps6-ll_valuebound5.c *)
@@ -291,11 +291,11 @@ struct
     let querycache = QueryHash.create 13 in
     query' ~querycache QuerySet.empty ctx q
 
-  and access (ctx:(D.t, G.t, C.t, V.t) ctx) e vo w: MCPAccess.A.t =
+  and access (ctx:(D.t, G.t, C.t, V.t) ctx) a: MCPAccess.A.t =
     let ctx'' = outer_ctx "access" ctx in
     let f (n, (module S: MCPSpec), d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "access" ctx'' n d in
-      (n, repr (S.access ctx' e vo w))
+      (n, repr (S.access ctx' a))
     in
     BatList.map f (spec_list ctx.local) (* map without deadcode *)
 
diff --git a/src/analyses/mHPAnalysis.ml b/src/analyses/mHPAnalysis.ml
index 0331057bc7..4a3af12a79 100644
--- a/src/analyses/mHPAnalysis.ml
+++ b/src/analyses/mHPAnalysis.ml
@@ -14,7 +14,7 @@ struct
     let should_print _ = true
   end
 
-  let access ctx e vo w: MHP.t =
+  let access ctx _: MHP.t =
     {
       tid = ctx.ask CurrentThreadId;
       created = ctx.ask CreatedThreads;
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 21bc76686b..e2cf12540e 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -162,11 +162,13 @@ struct
     let should_print ls = not (is_empty ls)
   end
 
-  let access ctx e vo w =
-    if w then
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point
+    | Memory {write = true; _} ->
       (* when writing: ignore reader locks *)
       Lockset.filter snd ctx.local
-    else
+    | Memory _ ->
       (* when reading: bump reader locks to exclusive as they protect reads *)
       Lockset.map (fun (x,_) -> (x,true)) ctx.local
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 9c326117de..01ba3ebf96 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -69,14 +69,18 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> true
   end
-  let access ctx e vo w =
-    (* TODO: remove regions that cannot be reached from the var*)
-    let rec unknown_index = function
-      | `NoOffset -> `NoOffset
-      | `Field (f, os) -> `Field (f, unknown_index os)
-      | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
-    in
-    Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point ->
+      Some (Lvals.empty ())
+    | Memory {exp = e; _} ->
+      (* TODO: remove regions that cannot be reached from the var*)
+      let rec unknown_index = function
+        | `NoOffset -> `NoOffset
+        | `Field (f, os) -> `Field (f, unknown_index os)
+        | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
+      in
+      Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index b4210516d6..3bf38fbf6b 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -197,8 +197,12 @@ struct
     Queries.ES.fold do_lockstep matching_exps
       (Queries.ES.fold do_perel matching_exps (A.empty ()))
 
-  let access ctx e vo w =
-    add_per_element_access ctx e false
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point ->
+      A.empty ()
+    | Memory {exp = e; _} ->
+      add_per_element_access ctx e false
 end
 
 let _ =
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 2f92d55d43..75b80d50a5 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -72,7 +72,7 @@ struct
     let may_race m1 m2 = m1 && m2 (* kill access when single threaded *)
     let should_print m = not m
   end
-  let access ctx e vo w =
+  let access ctx _ =
     is_multi (Analyses.ask_of_ctx ctx)
 
   let threadenter ctx lval f args =
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index aa0947e62b..00ddc5d6bc 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -104,7 +104,7 @@ struct
     let should_print = Option.is_some
   end
 
-  let access ctx e vo w =
+  let access ctx _ =
     if is_unique ctx then
       let tid = fst ctx.local in
       Some tid
diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml
index 607b3ab8f3..888477519e 100644
--- a/src/cdomains/deadlockDomain.ml
+++ b/src/cdomains/deadlockDomain.ml
@@ -1,24 +1,7 @@
 open Cil
 open Pretty
 
-type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : location}
+module Lock = LockDomain.Addr
+module LockEvent = Printable.Prod3 (Lock) (Node) (MCPAccess.A)
 
-
-module MyLock : Printable.S with type t = myowntypeEntry =
-struct
-  include Printable.Std (* for default invariant, tag, ... *)
-
-  type t = myowntypeEntry
-  module Ad = ValueDomain.Addr
-  let name () = "address with location"
-  let equal x y = Ad.equal x.addr y.addr (* ignores loc field *)
-  let hash x = Ad.hash x.addr
-  let compare x y = Ad.compare x.addr y.addr (* ignores loc field *)
-  (* TODO: deadlock analysis output doesn't even use these, but manually outputs locations *)
-  let show x = (Ad.show x.addr) ^ "@" ^ (CilType.Location.show x.loc)
-  let pretty () x = Ad.pretty () x.addr ++ text "@" ++ CilType.Location.pretty () x.loc
-  let printXml c x = Ad.printXml c x.addr
-  let to_yojson x = `String (show x)
-end
-
-module Lockset = SetDomain.ToppedSet (MyLock) (struct let topname = "all locks" end)
+module MayLockEvents = SetDomain.ToppedSet (LockEvent) (struct let topname = "All lock events" end)
diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index 86e7676097..9b4d773a3c 100644
--- a/src/cdomains/mHP.ml
+++ b/src/cdomains/mHP.ml
@@ -45,6 +45,12 @@ let definitely_not_started (current, created) other =
     else
       not @@ ConcDomain.ThreadSet.exists (ident_or_may_be_created) created
 
+let exists_definitely_not_started_in_joined (current,created) other_joined =
+  if ConcDomain.ThreadSet.is_top other_joined then
+    false
+  else
+    ConcDomain.ThreadSet.exists (definitely_not_started (current,created)) other_joined
+
 (** Must the thread with thread id other be already joined  *)
 let must_be_joined other joined =
   if ConcDomain.ThreadSet.is_top joined then
@@ -64,6 +70,8 @@ let may_happen_in_parallel one two =
       false
     else if must_be_joined tid2 must_joined || must_be_joined tid must_joined2 then
       false
+    else if exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined then
+      false
     else
       true
   | _ -> true
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 1dc44b3002..79cdefe96c 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -59,7 +59,11 @@ module Unit = Lattice.Unit
 type maybepublic = {global: CilType.Varinfo.t; write: bool} [@@deriving ord, hash]
 type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t} [@@deriving ord, hash]
 type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool} [@@deriving ord, hash]
-type partaccess = {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; write: bool} [@@deriving ord, hash]
+type memory_access = {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; write: bool} [@@deriving ord, hash]
+type access =
+  | Memory of memory_access (** Memory location access (race). *)
+  | Point (** Program point and state access (MHP), independent of memory location. *)
+[@@deriving ord, hash] (* TODO: fix ppx_deriving_hash on variant with inline record *)
 
 (** GADT for queries with specific result type. *)
 type _ t =
@@ -86,7 +90,7 @@ type _ t =
   | BlobSize: exp -> ID.t t (* size of a dynamically allocated `Blob pointed to by exp *)
   | PrintFullState: Unit.t t
   | CondVars: exp -> ES.t t
-  | PartAccess: partaccess -> Obj.t t (** Only queried by access analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *)
+  | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *)
   | IterPrevVars: iterprevvar -> Unit.t t
   | IterVars: itervar -> Unit.t t
   | MustBeEqual: exp * exp -> MustBool.t t (* are two expression known to must-equal ? *)
@@ -273,7 +277,7 @@ struct
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
       | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2
       | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2
-      | Any (PartAccess p1), Any (PartAccess p2) -> compare_partaccess p1 p2
+      | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2
       | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2
       | Any (IterVars i1), Any (IterVars i2) -> compare_itervar i1 i2
       | Any (MustBeEqual (e1, e2)), Any (MustBeEqual (e3, e4)) ->
@@ -308,7 +312,7 @@ struct
     | Any (EvalLength e) -> CilType.Exp.hash e
     | Any (BlobSize e) -> CilType.Exp.hash e
     | Any (CondVars e) -> CilType.Exp.hash e
-    | Any (PartAccess p) -> hash_partaccess p
+    | Any (PartAccess p) -> hash_access p
     | Any (IterPrevVars i) -> 0
     | Any (IterVars i) -> 0
     | Any (MustBeEqual (e1, e2)) -> [%hash: CilType.Exp.t * CilType.Exp.t] (e1, e2)
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index d6244d60e1..f7b4e40efd 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -391,7 +391,7 @@ sig
   val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
 
   module A: MCPA
-  val access: (D.t, G.t, C.t, V.t) ctx -> exp -> varinfo option -> bool -> A.t
+  val access: (D.t, G.t, C.t, V.t) ctx -> Queries.access -> A.t
 end
 
 type analyzed_data = {
@@ -569,7 +569,7 @@ struct
   (* Everything is context sensitive --- override in MCP and maybe elsewhere*)
 
   module A = UnitA
-  let access _ _ _ _ = ()
+  let access _ _ = ()
 end
 
 (* Even more default implementations. Most transfer functions acting as identity functions. *)
diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index f644c0ac1f..cbfc643409 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -27,6 +27,7 @@ type category =
   | Behavior of behavior
   | Integer of integer
   | Race
+  | Deadlock
   | Cast of cast
   | Deadcode
   | Unknown
@@ -160,6 +161,7 @@ let should_warn e =
     | Behavior _ -> "behavior"
     | Integer _ -> "integer"
     | Race -> "race"
+    | Deadlock -> "deadlock"
     | Cast _ -> "cast"
     | Deadcode -> "deadcode"
     | Unknown -> "unknown"
@@ -174,6 +176,7 @@ let path_show e =
   | Behavior x -> "Behavior" :: Behavior.path_show x
   | Integer x -> "Integer" :: Integer.path_show x
   | Race -> ["Race"]
+  | Deadlock -> ["Deadlock"]
   | Cast x -> "Cast" :: Cast.path_show x
   | Deadcode -> ["Deadcode"]
   | Unknown -> ["Unknown"]
@@ -197,6 +200,7 @@ let categoryName = function
   | Assert -> "Assert"
 
   | Race -> "Race"
+  | Deadlock -> "Deadlock"
   | Cast x -> "Cast"
   | Deadcode -> "Deadcode"
   | Unknown -> "Unknown"
@@ -218,6 +222,7 @@ let from_string_list (s: string list) =
     | "behavior" -> Behavior.from_string_list t
     | "integer" -> Integer.from_string_list t
     | "race" -> Race
+    | "deadlock" -> Deadlock
     | "cast" -> Cast.from_string_list t
     | "deadcode" -> Deadcode
     | "analyzer" -> Analyzer
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 9f114ec749..4edff233e0 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1575,6 +1575,12 @@
           "type": "boolean",
           "default": true
         },
+        "deadlock": {
+          "title": "warn.deadlock",
+          "description": "Deadlock warnings",
+          "type": "boolean",
+          "default": true
+        },
         "deadcode": {
           "title": "warn.deadcode",
           "description": "Dead code warnings",
diff --git a/tests/regression/15-deadlock/01-basic_deadlock.c b/tests/regression/15-deadlock/01-basic_deadlock.c
index a0cce14b45..84bd44b00a 100644
--- a/tests/regression/15-deadlock/01-basic_deadlock.c
+++ b/tests/regression/15-deadlock/01-basic_deadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
   pthread_mutex_lock(&mutex2); // DEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -16,7 +16,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex2);
+  pthread_mutex_lock(&mutex2); // DEADLOCK
   pthread_mutex_lock(&mutex1); // DEADLOCK
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
diff --git a/tests/regression/15-deadlock/02-basic_nodeadlock.c b/tests/regression/15-deadlock/02-basic_nodeadlock.c
index 66de92c652..97d9992b42 100644
--- a/tests/regression/15-deadlock/02-basic_nodeadlock.c
+++ b/tests/regression/15-deadlock/02-basic_nodeadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex2); // NODEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -16,7 +16,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex2); // NODEADLOCK
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex2);
diff --git a/tests/regression/15-deadlock/03-triple_deadlock.c b/tests/regression/15-deadlock/03-triple_deadlock.c
index abff21b16d..7ba5cdabd5 100644
--- a/tests/regression/15-deadlock/03-triple_deadlock.c
+++ b/tests/regression/15-deadlock/03-triple_deadlock.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] deadlock
+// PARAM: --set ana.activated[+] deadlock
 #include <pthread.h>
 #include <stdio.h>
 
@@ -8,7 +8,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
   pthread_mutex_lock(&mutex2); // DEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -17,7 +17,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex2);
+  pthread_mutex_lock(&mutex2); // DEADLOCK
   pthread_mutex_lock(&mutex3); // DEADLOCK
   g2 = g3 - 1;
   pthread_mutex_unlock(&mutex3);
@@ -26,7 +26,7 @@ void *t2(void *arg) {
 }
 
 void *t3(void *arg) {
-  pthread_mutex_lock(&mutex3);
+  pthread_mutex_lock(&mutex3); // DEADLOCK
   pthread_mutex_lock(&mutex1); // DEADLOCK
   g3 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
diff --git a/tests/regression/15-deadlock/04-triple_nodeadlock.c b/tests/regression/15-deadlock/04-triple_nodeadlock.c
index 8849c642e4..89883f4995 100644
--- a/tests/regression/15-deadlock/04-triple_nodeadlock.c
+++ b/tests/regression/15-deadlock/04-triple_nodeadlock.c
@@ -8,7 +8,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1);  // NODEADLOCK
   pthread_mutex_lock(&mutex2);  // NODEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -17,7 +17,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex2);
+  pthread_mutex_lock(&mutex2); // NODEADLOCK
   pthread_mutex_lock(&mutex3); // NODEADLOCK
   g2 = g3 - 1;
   pthread_mutex_unlock(&mutex3);
@@ -26,7 +26,7 @@ void *t2(void *arg) {
 }
 
 void *t3(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex3); // NODEADLOCK
   g3 = g1 + 1;
   pthread_mutex_unlock(&mutex3);
diff --git a/tests/regression/15-deadlock/05-may_deadlock.c b/tests/regression/15-deadlock/05-may_deadlock.c
index 99f95093b0..04673eba27 100644
--- a/tests/regression/15-deadlock/05-may_deadlock.c
+++ b/tests/regression/15-deadlock/05-may_deadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
   pthread_mutex_lock(&mutex2); // DEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -18,7 +18,7 @@ void *t1(void *arg) {
 void *t2(void *arg) {
   int k = rand() % 2;
   if (k)
-    pthread_mutex_lock(&mutex2);
+    pthread_mutex_lock(&mutex2); // DEADLOCK
   pthread_mutex_lock(&mutex1); // DEADLOCK
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
diff --git a/tests/regression/15-deadlock/06-may_nodeadlock.c b/tests/regression/15-deadlock/06-may_nodeadlock.c
index cc79c795a3..8656de4c85 100644
--- a/tests/regression/15-deadlock/06-may_nodeadlock.c
+++ b/tests/regression/15-deadlock/06-may_nodeadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex2); // NODEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -18,7 +18,7 @@ void *t1(void *arg) {
 void *t2(void *arg) {
   int k = rand() % 2;
   if (k)
-    pthread_mutex_lock(&mutex2);
+    pthread_mutex_lock(&mutex2); // NODEADLOCK
   else
     pthread_mutex_lock(&mutex1); // NODEADLOCK
   g2 = g1 + 1;
diff --git a/tests/regression/15-deadlock/07-account_deadlock.c b/tests/regression/15-deadlock/07-account_deadlock.c
index bfa4661a36..7819cc51eb 100644
--- a/tests/regression/15-deadlock/07-account_deadlock.c
+++ b/tests/regression/15-deadlock/07-account_deadlock.c
@@ -10,7 +10,7 @@ typedef struct {
 bank_account A, B;
 
 void deposit(bank_account *f, bank_account *t, int ammount) {
-  pthread_mutex_lock(&f->mutex);
+  pthread_mutex_lock(&f->mutex);  // DEADLOCK
   pthread_mutex_lock(&t->mutex);  // DEADLOCK
   t->balance += ammount;
   f->balance -= ammount;
diff --git a/tests/regression/15-deadlock/08-account_nodeadlock.c b/tests/regression/15-deadlock/08-account_nodeadlock.c
index 36e0996cce..74252d9380 100644
--- a/tests/regression/15-deadlock/08-account_nodeadlock.c
+++ b/tests/regression/15-deadlock/08-account_nodeadlock.c
@@ -10,7 +10,7 @@ typedef struct {
 bank_account A, B;
 
 void deposit(bank_account *f, bank_account *t, int ammount) {
-  pthread_mutex_lock(&f->mutex);
+  pthread_mutex_lock(&f->mutex);  // NODEADLOCK
   pthread_mutex_lock(&t->mutex);  // NODEADLOCK
   t->balance += ammount;
   f->balance -= ammount;
diff --git a/tests/regression/15-deadlock/09-account_correct.c b/tests/regression/15-deadlock/09-account_correct.c
index 305a4d8428..617003b106 100644
--- a/tests/regression/15-deadlock/09-account_correct.c
+++ b/tests/regression/15-deadlock/09-account_correct.c
@@ -23,10 +23,10 @@ void deposit(bank_account *f, bank_account *t, int ammount) {
     return;
 
   if (f->id < t->id) {
-    pthread_mutex_lock(&f->mutex);
+    pthread_mutex_lock(&f->mutex); // NODEADLOCK
     pthread_mutex_lock(&t->mutex); // NODEADLOCK
   } else {
-    pthread_mutex_lock(&t->mutex);
+    pthread_mutex_lock(&t->mutex); // NODEADLOCK
     pthread_mutex_lock(&f->mutex); // NODEADLOCK
   }
 
diff --git a/tests/regression/15-deadlock/10-account_incorrect.c b/tests/regression/15-deadlock/10-account_incorrect.c
index 8c532fdfc8..a6a7b75da3 100644
--- a/tests/regression/15-deadlock/10-account_incorrect.c
+++ b/tests/regression/15-deadlock/10-account_incorrect.c
@@ -23,10 +23,10 @@ void deposit(bank_account *f, bank_account *t, int ammount) {
     return;
 
   if (f->id < t->id) {
-    pthread_mutex_lock(&f->mutex);
+    pthread_mutex_lock(&f->mutex); // DEADLOCK
     pthread_mutex_lock(&t->mutex); // DEADLOCK
   } else {
-    pthread_mutex_lock(&f->mutex);
+    pthread_mutex_lock(&f->mutex); // DEADLOCK
     pthread_mutex_lock(&t->mutex); // DEADLOCK
   }
 
diff --git a/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c b/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c
new file mode 100644
index 0000000000..ef23346ade
--- /dev/null
+++ b/tests/regression/15-deadlock/11-common_mutex_nodeadlock.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(&mutex3); // NODEADLOCK
+  pthread_mutex_lock(&mutex1); // NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex2); // NODEADLOCK (common mutex3)
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_mutex_lock(&mutex3); // NODEADLOCK
+  pthread_mutex_lock(&mutex2); // NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex1); // NODEADLOCK (common mutex3)
+  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/12-ase16_nodeadlock.c b/tests/regression/15-deadlock/12-ase16_nodeadlock.c
new file mode 100644
index 0000000000..1cbdf2e704
--- /dev/null
+++ b/tests/regression/15-deadlock/12-ase16_nodeadlock.c
@@ -0,0 +1,65 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+// From https://arxiv.org/abs/1607.06927
+#include <pthread.h>
+
+int x;
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
+
+void func1() {
+  x = 0; // RACE!
+}
+
+int func2(int a) {
+  pthread_mutex_lock(&m5); // NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m4); // NODEADLOCK (thread joined)
+  if (a)
+    x = 3; // NORACE (thread joined)
+  else
+    x = 4;
+  pthread_mutex_unlock(&m4);
+  pthread_mutex_unlock(&m5);
+  return 0;
+}
+
+void *thread() {
+  pthread_mutex_lock(&m1); // NODEADLOCK
+  pthread_mutex_lock(&m2); // NODEADLOCK (common m1)
+  pthread_mutex_lock(&m3); // NODEADLOCK (common m1)
+  x = 1; // NORACE (thread joined)
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m1);
+
+  pthread_mutex_lock(&m4); // NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m5); // NODEADLOCK (thread joined)
+  x = 2; // RACE!
+  pthread_mutex_unlock(&m5);
+  pthread_mutex_unlock(&m4);
+
+  return NULL;
+}
+
+int main() {
+  pthread_t tid;
+
+  pthread_create(&tid, NULL, thread, NULL);
+
+  pthread_mutex_lock(&m1); // NODEADLOCK
+  pthread_mutex_lock(&m3); // NODEADLOCK (common m1)
+  pthread_mutex_lock(&m2); // NODEADLOCK (common m1)
+  func1();
+  pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m1);
+
+  pthread_join(tid, NULL);
+
+  int r;
+  r = func2(5);
+
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/13-deadlock-mhp.c b/tests/regression/15-deadlock/13-deadlock-mhp.c
new file mode 100644
index 0000000000..c31a174863
--- /dev/null
+++ b/tests/regression/15-deadlock/13-deadlock-mhp.c
@@ -0,0 +1,31 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+#include <pthread.h>
+
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *thread() {
+  pthread_mutex_lock(&m2); //DEADLOCK
+  pthread_mutex_lock(&m1); //DEADLOCK
+  pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m1);
+
+  return NULL;
+}
+
+void *noOpThread() {
+  return NULL;
+}
+
+int main() {
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, NULL, noOpThread, NULL);
+
+  pthread_mutex_lock(&m1); // DEADLOCK
+  pthread_create(&tid2, NULL, thread, NULL);
+  pthread_mutex_lock(&m2); //DEADLOCK
+
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/14-missing-unlock.c b/tests/regression/15-deadlock/14-missing-unlock.c
new file mode 100644
index 0000000000..6381da08c5
--- /dev/null
+++ b/tests/regression/15-deadlock/14-missing-unlock.c
@@ -0,0 +1,33 @@
+// SKIP PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+// TODO: https://github.com/goblint/analyzer/issues/667
+#include <pthread.h>
+
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *thread() {
+  pthread_mutex_lock(&m2);
+  pthread_mutex_lock(&m1);
+  // We forgot to unlock
+  // pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m1);
+
+  return NULL;
+}
+
+void *noOpThread() {
+  return NULL;
+}
+
+int main() {
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, NULL, noOpThread, NULL);
+
+  pthread_create(&tid2, NULL, thread, NULL);
+  pthread_join(tid2,NULL);
+  pthread_mutex_lock(&m2); // TODO DEADLOCK
+
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/15-deadlock-mhp2.c b/tests/regression/15-deadlock/15-deadlock-mhp2.c
new file mode 100644
index 0000000000..5ef912400c
--- /dev/null
+++ b/tests/regression/15-deadlock/15-deadlock-mhp2.c
@@ -0,0 +1,64 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+#include <pthread.h>
+
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
+pthread_t decoy;
+
+
+void *noOpThread() {
+  return NULL;
+}
+
+void *thread2() {
+  pthread_mutex_lock(&m3); // NODEADLOCK (decoy not yet created)
+  pthread_mutex_lock(&m1); // NODEADLOCK (decoy not yet created)
+
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m1);
+
+  return NULL;
+}
+
+void *thread() {
+  pthread_mutex_lock(&m2); // NODEADLOCK (decoy not yet created)
+  pthread_mutex_lock(&m3); // NODEADLOCK (decoy not yet created)
+
+  pthread_mutex_lock(&m4); // NODEADLOCK (not in cycle)
+  pthread_create(&decoy, NULL, noOpThread, NULL);
+  pthread_mutex_unlock(&m4);
+
+
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m2);
+
+  return NULL;
+}
+
+int main() {
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, NULL, thread, NULL);
+  pthread_create(&tid2, NULL, thread2, NULL);
+
+  pthread_mutex_lock(&m1); // NODEADLOCK (decoy not yet created)
+
+  pthread_mutex_lock(&m4); // NODEADLOCK (not in cycle)
+  pthread_t dec = decoy;
+  pthread_mutex_unlock(&m4);
+
+  if(dec != NULL) {
+    pthread_join(dec,NULL);
+    pthread_mutex_lock(&m2); // NODEADLOCK (decoy not yet created)
+
+    pthread_mutex_unlock(&m1);
+    pthread_mutex_unlock(&m2);
+  } else {
+    pthread_mutex_unlock(&m1);
+  }
+
+  return 0;
+}