BSc thesis "Coloring Data Race Interference Graphs"

dune-project

@@ -41,6 +41,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (goblint-cil (>= 2.1.0)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.9.0))
     (patricia-tree (>= 0.14.0))
+    ocamlgraph
     (zarith (>= 1.12))
     (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
     (qcheck-core (>= 0.90))

goblint.opam

@@ -42,6 +42,7 @@ depends: [
   "goblint-cil" {>= "2.1.0"}
   "batteries" {>= "3.9.0"}
   "patricia-tree" {>= "0.14.0"}
+  "ocamlgraph"
   "zarith" {>= "1.12"}
   "yojson" {>= "2.0.0" & < "3"}
   "qcheck-core" {>= "0.90"}

goblint.opam.locked

@@ -93,6 +93,7 @@ depends: [
   "ocamlc-loc" {= "3.21.1" & with-dev-setup}
   "ocamlfind" {= "1.9.8"}
   "ocamlformat-rpc-lib" {= "0.29.0" & with-dev-setup}
+  "ocamlgraph" {= "2.2.0"}
   "ocp-indent" {= "1.8.1" & with-dev-setup}
   "odoc" {= "3.0.0" & with-doc}
   "odoc-parser" {= "3.0.0" & with-doc}

scripts/goblint-lib-modules.py

@@ -12,6 +12,7 @@
     src_root_path / "util" / "parallel" / "goblint_parallel.ml",
     src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
+    src_root_path / "util" / "ocamlgraph" / "goblint_ocamlgraph.ml",
 ]
 goblint_lib_modules = set()
 
@@ -39,6 +40,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_ocamlgraph",
     "Goblint_constraint",
     "Goblint_parallel",
     "Goblint_solver",

src/config/options.schema.json

@@ -2463,6 +2463,13 @@
           "type": "integer",
           "default": 0
         },
+        "race-coloring": {
+          "title": "warn.race-coloring",
+          "description": "Group race warnings by graph coloring (none, greedy, dsatur, rlf, optimal).",
+          "type": "string",
+          "enum": ["none", "greedy", "dsatur", "rlf", "optimal"],
+          "default": "none"
+        },
         "deterministic": {
           "title": "warn.deterministic",
           "description": "Output messages in deterministic order. Useful for cram testing.",

src/domains/access.ml

@@ -594,6 +594,40 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
   | Some n when n >= 100 -> is_all_safe := false; incr unsafe
   | Some n -> is_all_safe := false; incr vulnerable
 
+module InterferenceGraph =
+struct
+  include Graph.Imperative.Graph.Concrete (A)
+
+  let of_accesses (accs : AS.t) =
+    let graph = create () in
+    AS.iter (fun acc -> add_vertex graph acc) accs;
+    let accs_list = AS.elements accs in
+    let rec loop = function
+      | [] -> ()
+      | a :: rest ->
+        List.iter (fun b ->
+            if may_race a b then
+              add_edge graph a b
+          ) rest;
+        loop rest
+    in
+    loop accs_list;
+    graph
+end
+module InterferenceGraphColoring = Goblint_ocamlgraph.Coloring.Make (InterferenceGraph)
+
+let coloring_module =
+  lazy (
+    let open InterferenceGraphColoring in
+    match get_string "warn.race-coloring" with
+    | "none" -> None
+    | "greedy" -> Some (module Greedy: ALGORITHM)
+    | "dsatur" -> Some (module Dsatur)
+    | "rlf" -> Some (module Rlf)
+    | "optimal" -> Some (module Optimal)
+    | _ -> assert false
+  )
+
 let print_accesses memo grouped_accs =
   let allglobs = get_bool "allglobs" in
   let race_threshold = get_int "warn.race-threshold" in
@@ -602,8 +636,30 @@ let print_accesses memo grouped_accs =
       let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
-    AS.elements race_accs
-    |> List.map h
+    match coloring_module with
+    | lazy None ->
+      AS.elements race_accs
+      |> List.map h
+    | lazy (Some (module Coloring: InterferenceGraphColoring.ALGORITHM)) ->
+      let graph = InterferenceGraph.of_accesses race_accs in
+      let coloring = Coloring.color graph in
+      let module IntMap = Map.Make (Int) in
+      let add_to_map acc map =
+        match InterferenceGraphColoring.color_of coloring acc with
+        | None -> map
+        | Some c ->
+          IntMap.update c (function
+              | None -> Some [acc]
+              | Some accs -> Some (acc :: accs)
+            ) map
+      in
+      let color_map = AS.fold add_to_map race_accs IntMap.empty in
+      IntMap.bindings color_map
+      |> List.concat_map (fun (color, accs) ->
+          let header = (dprintf "Color %d" color, None) in
+          let acc_msgs = accs |> List.rev |> List.map h in
+          header :: acc_msgs
+        )
   in
   let group_loc = match memo with
     | (`Var v, _) -> Some (M.Location.CilLocation v.vdecl) (* TODO: offset location *)

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint goblint_memtrace privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
+  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common ocamlgraph goblint_ocamlgraph goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies

src/index.mld

@@ -40,6 +40,9 @@ The following libraries provide extensions to other OCaml libraries.
 {2 Library goblint.std}
 {!modules:Goblint_std}
 
+{2 Library goblint.ocamlgraph}
+{!modules:Goblint_ocamlgraph}
+
 
 {1 Package utilities}
 The following libraries provide [goblint] package metadata for executables.

src/util/ocamlgraph/coloring.ml

@@ -0,0 +1,213 @@
+module Make (G : Graph.Coloring.G) = struct
+  module C = Graph.Coloring.Make (G)
+  module IntSet = Set.Make (Int)
+
+  type coloring = int C.H.t
+
+  module type ALGORITHM = sig
+    val color : G.t -> coloring
+  end
+
+  let k_color g k = C.coloring g k
+  let color_with (module A : ALGORITHM) g = A.color g
+  let color_of coloring v = C.H.find_opt coloring v
+  let colors_used coloring = C.H.fold (fun _ c acc -> max acc c) coloring 0
+
+  module Greedy : ALGORITHM = struct
+    let color g =
+      let n = G.nb_vertex g in
+      let coloring = C.H.create n in
+      let vertices =
+        G.fold_vertex (fun v acc -> (G.out_degree g v, v) :: acc) g []
+        |> List.sort (fun (d1, _) (d2, _) -> compare d2 d1)
+        |> List.map snd
+      in
+      let next_color v =
+        let used = ref IntSet.empty in
+        G.iter_succ (fun u ->
+            match C.H.find_opt coloring u with
+            | None -> ()
+            | Some c -> used := IntSet.add c !used
+          ) g v;
+        let rec pick c =
+          if IntSet.mem c !used then
+            pick (c + 1)
+          else
+            c
+        in
+        pick 1
+      in
+      List.iter (fun v -> C.H.add coloring v (next_color v)) vertices;
+      coloring
+  end
+
+  module Optimal : ALGORITHM = struct
+    let color g =
+      let max_colors = max 1 (G.nb_vertex g) in
+      let rec loop k =
+        if k > max_colors then
+          raise Graph.Coloring.NoColoring
+        else
+          try C.coloring g k with
+          | Graph.Coloring.NoColoring -> loop (k + 1)
+      in
+      loop 1
+  end
+
+  module Dsatur : ALGORITHM = struct
+    let color g =
+      let n = G.nb_vertex g in
+      let coloring = C.H.create n in
+      let saturation = C.H.create n in
+      let degree = C.H.create n in
+      G.iter_vertex (fun v ->
+          C.H.replace saturation v IntSet.empty;
+          C.H.replace degree v (G.out_degree g v)
+        ) g;
+      let is_colored v = C.H.mem coloring v in
+      let sat_count v =
+        match C.H.find_opt saturation v with
+        | None -> 0
+        | Some s -> IntSet.cardinal s
+      in
+      let choose_vertex () =
+        let pick v best_opt =
+          if is_colored v then
+            best_opt
+          else
+            match best_opt with
+            | None -> Some v
+            | Some best ->
+              let sv = sat_count v in
+              let sb = sat_count best in
+              if sv > sb then
+                Some v
+              else if sv < sb then
+                Some best
+              else (
+                let dv = C.H.find degree v in
+                let db = C.H.find degree best in
+                if dv > db then Some v else Some best
+              )
+        in
+        G.fold_vertex pick g None
+      in
+      let pick_color v =
+        let used =
+          match C.H.find_opt saturation v with
+          | None -> IntSet.empty
+          | Some s -> s
+        in
+        let rec pick c =
+          if IntSet.mem c used then
+            pick (c + 1)
+          else
+            c
+        in
+        pick 1
+      in
+      let rec loop () =
+        match choose_vertex () with
+        | None -> ()
+        | Some v ->
+          let c = pick_color v in
+          C.H.add coloring v c;
+          G.iter_succ (fun u ->
+              if not (is_colored u) then
+                let s =
+                  match C.H.find_opt saturation u with
+                  | None -> IntSet.empty
+                  | Some s -> s
+                in
+                C.H.replace saturation u (IntSet.add c s)
+            ) g v;
+          loop ()
+      in
+      loop ();
+      coloring
+  end
+
+  module Rlf : ALGORITHM = struct
+    module VSet = struct
+      let create n = C.H.create n
+      let mem s v = C.H.mem s v
+      let add s v = C.H.replace s v ()
+      let remove s v = C.H.remove s v
+    end
+
+    let color g =
+      let n = G.nb_vertex g in
+      let coloring = C.H.create n in
+      let uncolored = VSet.create n in
+      G.iter_vertex (fun v -> VSet.add uncolored v) g;
+      let degree v = G.out_degree g v in
+      let pick_start () =
+        G.fold_vertex (fun v best ->
+            if not (VSet.mem uncolored v) then
+              best
+            else
+              match best with
+              | None -> Some v
+              | Some b ->
+                if degree v > degree b then Some v else Some b
+          ) g None
+      in
+      let add_forbidden forbidden v =
+        G.iter_succ (fun u ->
+            if VSet.mem uncolored u then
+              VSet.add forbidden u
+          ) g v
+      in
+      let candidate_score forbidden v =
+        let count = ref 0 in
+        G.iter_succ (fun u ->
+            if VSet.mem forbidden u then
+              incr count
+          ) g v;
+        !count
+      in
+      let pick_candidate forbidden =
+        G.fold_vertex (fun v best ->
+            if not (VSet.mem uncolored v) || VSet.mem forbidden v then
+              best
+            else
+              match best with
+              | None -> Some v
+              | Some b ->
+                let sv = candidate_score forbidden v in
+                let sb = candidate_score forbidden b in
+                if sv > sb then
+                  Some v
+                else if sv < sb then
+                  Some b
+                else if degree v > degree b then
+                  Some v
+                else
+                  Some b
+          ) g None
+      in
+      let rec color_class color =
+        match pick_start () with
+        | None -> ()
+        | Some v0 ->
+          let forbidden = VSet.create n in
+          let add_vertex v =
+            C.H.add coloring v color;
+            VSet.remove uncolored v;
+            add_forbidden forbidden v
+          in
+          add_vertex v0;
+          let rec fill () =
+            match pick_candidate forbidden with
+            | None -> ()
+            | Some v ->
+              add_vertex v;
+              fill ()
+          in
+          fill ();
+          color_class (color + 1)
+      in
+      color_class 1;
+      coloring
+  end
+end

src/util/ocamlgraph/dune

@@ -0,0 +1,8 @@
+(include_subdirs no)
+
+(library
+ (name goblint_ocamlgraph)
+ (public_name goblint.ocamlgraph)
+ (libraries
+   ocamlgraph)
+ (instrumentation (backend bisect_ppx)))

src/util/ocamlgraph/goblint_ocamlgraph.ml

@@ -0,0 +1,3 @@
+(** OCamlgraph library extensions which are completely independent of Goblint. *)
+
+module Coloring = Coloring