Analysis of pthread_barriers

.github/workflows/coverage.yml

@@ -46,6 +46,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Install coverage dependencies
         run: opam install bisect_ppx
 

.github/workflows/locked.yml

@@ -48,6 +48,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
@@ -100,6 +103,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 

.github/workflows/unlocked.yml

@@ -57,6 +57,9 @@ jobs:
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
+
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
 
       - name: Install Apron dependencies
         if: ${{ matrix.apron }}
@@ -118,6 +121,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Install Apron dependencies
         run: |
           opam depext apron

make.sh

@@ -75,7 +75,7 @@ rule() {
     ;; setup)
       echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config"
       echo "For the --html output you also need: javac, ant, dot (graphviz)"
-      echo "For running the regression tests you also need: ruby, gem, curl"
+      echo "For running the regression tests you also need: ruby, gem, curl, and the `os` gem"
       echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
       opam_setup
     ;; dev)
@@ -90,6 +90,7 @@ rule() {
       # Use `git commit -n` to temporarily bypass the hook if necessary.
       echo "Installing gem parallel (not needed for ./scripts/update_suite.rb -s)"
       sudo gem install parallel
+      sudo gem install os
     ;; headers)
       curl -L -O https://github.com/goblint/linux-headers/archive/master.tar.gz
       tar xf master.tar.gz && rm master.tar.gz

scripts/update_suite.rb

@@ -575,6 +575,15 @@ def run ()
     end
 end
 
+maybemac = true
+
+begin
+    require 'os'
+    maybemac = OS.mac?
+rescue LoadError => e
+    puts "Missing os gem (install with: gem install os), skipping tests that do not work on mac"
+end
+
 #processing the file information
 projects = []
 project_ids = Set.new
@@ -603,6 +612,7 @@ def run ()
     lines = IO.readlines(path, :encoding => "UTF-8")
 
     next if not future and only.nil? and lines[0] =~ /SKIP/
+    next if maybemac and lines[0] =~ /NOMAC/
     next if marshal and lines[0] =~ /NOMARSHAL/
     next if not has_linux_headers and lines[0] =~ /kernel/
     if incremental then

src/analyses/pthreadBarriers.ml

@@ -0,0 +1,167 @@
+(** Must have waited barriers for Pthread barriers ([pthreadBarriers]). *)
+
+open GoblintCil
+open Analyses
+module LF = LibraryFunctions
+
+module Spec =
+struct
+  module Barriers = struct
+    include SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All barriers" end)
+    let name () = "mayBarriers"
+  end
+
+  module MustBarriers = struct
+    include Lattice.Reverse (Barriers)
+    let name () = "mustBarriers"
+  end
+
+  module Capacity = Queries.ID
+
+  include Analyses.IdentitySpec
+  module V = VarinfoV
+
+  module TID = ThreadIdDomain.ThreadLifted
+
+  module MHPplusLock = struct
+    module Locks = LockDomain.MustLockset
+
+    include Printable.Prod (MHP) (Locks)
+    let name () = "MHPplusLock"
+
+    let mhp (mhp1, l1) (mhp2, l2) =
+      MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2)
+
+    let tid ((mhp:MHP.t), _) = mhp.tid
+
+    let may_be_non_unique_thread (mhp, _) = MHP.may_be_non_unique_thread mhp
+  end
+
+  module Waiters = SetDomain.ToppedSet (MHPplusLock) (struct let topname = "All MHP" end)
+  module Multiprocess = BoolDomain.MayBool
+  module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters)
+
+  let name () = "pthreadBarriers"
+
+  module MustObserved = MapDomain.MapTop_LiftBot (TID) (MustBarriers)
+  module D = Lattice.Prod (Barriers) (MustObserved)
+
+  include Analyses.ValueContexts(D)
+
+  let possible_vinfos (a: Queries.ask) barrier =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
+
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let exists_k pred k waiters =
+      let k_product elems =
+        let rec doit k =
+          if k = 1 then
+            Seq.map (Seq.return) elems
+          else
+            let arg = doit (k-1) in
+            Seq.map_product (Seq.cons) elems arg
+        in
+        doit k
+      in
+      Seq.exists pred (k_product (Waiters.to_seq waiters))
+    in
+    let desc = LF.find f in
+    match desc.special arglist with
+    | BarrierWait barrier ->
+      let ask = Analyses.ask_of_man man in
+      let may, must = man.local in
+      let barriers = possible_vinfos ask barrier in
+      let mhp = MHP.current ask in
+      let handle_one b =
+        try
+          let locks = man.ask (Queries.MustLockset) in
+          man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
+          let addr = ValueDomain.Addr.of_var b in
+          let (multiprocess, capacity, waiters) = man.global b in
+          let may = Barriers.add addr may in
+          if multiprocess then
+            (may, must)
+          else
+            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in
+            if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then
+              (may, must)
+            else
+              match capacity with
+              | `Top | `Bot -> (may, must)
+              | `Lifted c ->
+                let count = Waiters.cardinal relevant_waiters in
+                (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
+                let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
+                if Z.leq min_cap Z.one then
+                  (may, must)
+                else if Z.geq (Z.of_int (count + 1)) min_cap then
+                  (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that
+                      MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                      better algorithmically (beyond just laziness) *)
+                  let must =
+                    let waiters = Waiters.elements relevant_waiters in
+                    let min_cap = Z.to_int min_cap in
+                    let can_proceed_pred seq =
+                      let rec doit seq = match Seq.uncons seq with
+                        | None -> true
+                        | Some (h, t) -> Seq.for_all (MHPplusLock.mhp h) t && doit t
+                      in
+                      doit seq
+                    in
+                    let can_proceed = exists_k can_proceed_pred (min_cap - 1) relevant_waiters in
+                    if not can_proceed then raise Analyses.Deadcode;
+                    (* limit to this case to avoid having to construct all permutations above *)
+                    if BatList.compare_length_with waiters (min_cap - 1) = 0 then
+                      List.fold_left (fun acc elem ->
+                          let tid = MHPplusLock.tid elem in
+                          let curr = MustObserved.find tid acc in
+                          let must' = MustObserved.add tid (Barriers.add addr curr) acc in
+                          must'
+                        ) must waiters
+                    else
+                      must
+                  in
+                  (may, must)
+                else
+                  raise Analyses.Deadcode;
+        with Analyses.Deadcode -> D.bot ()
+      in
+      let (may, must) = List.fold_left (fun acc b-> D.join acc (handle_one b)) (D.bot ()) barriers in
+      if Barriers.is_empty may then raise Analyses.Deadcode;
+      (may, must)
+    | BarrierInit { barrier; attr; count } ->
+      let multitprocess = not @@ Queries.AD.is_null @@ man.ask (Queries.MayPointTo attr) in
+      if multitprocess then M.warn "Barrier initialized with a non-NULL attr argument. Handled as if PTHREAD_PROCESS_SHARED potentially set.";
+      let count = man.ask (Queries.EvalInt count) in
+      let publish_one b = man.sideg b (multitprocess, count, Waiters.bot ()) in
+      let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
+      List.iter publish_one barriers;
+      man.local
+    | _ -> man.local
+
+  let startstate v = (Barriers.empty (), MustObserved.empty ())
+  let threadenter man ~multiple lval f args = [man.local]
+  let exitstate  v = (Barriers.empty (), MustObserved.empty ())
+
+  module A =
+  struct
+    include Lattice.Prod3 (Barriers) (MustObserved) (TID)
+    let name () = "barriers"
+    let may_race (may_await_t1, must_observed_by_t1, t1) (may_await_t2, must_observed_by_t2, t2) =
+      let observed_from_t2 = MustObserved.find t2 must_observed_by_t1 in
+      if not (Barriers.subset observed_from_t2 may_await_t2) then
+        false
+      else
+        let observed_from_t1 = MustObserved.find t1 must_observed_by_t2 in
+        Barriers.subset observed_from_t1 may_await_t1
+    let should_print f = true
+  end
+
+  let access man (a: Queries.access) =
+    let (may,must) = man.local in
+    let mhp = MHP.current (Analyses.ask_of_man man) in
+    (may, must, mhp.tid)
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/cdomains/mHP.ml

@@ -92,3 +92,8 @@ let may_happen_in_parallel one two =
     else
       true
   | _ -> true
+
+let may_be_non_unique_thread mhp =
+  match mhp.tid with
+  | `Lifted tid -> not (TID.is_unique tid)
+  | _ -> true

src/domain/disjointDomain.ml

@@ -117,6 +117,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f m = fold (fun e acc ->
       add (f e) acc
     ) m (empty ()) (* no intermediate lists *)
@@ -323,6 +324,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f s = fold (fun e acc ->
       add (f e) acc
     ) s (empty ()) (* no intermediate lists *)

src/domain/setDomain.ml

@@ -95,6 +95,12 @@ sig
       On set abstractions this lists only canonical elements,
       not all subsumed elements. *)
 
+  val to_seq: t -> elt Seq.t
+  (** See {!Set.S.to_seq}.
+
+      On set abstractions this lists only canonical elements,
+      not all subsumed elements. *)
+
   val of_list: elt list -> t
 
   val min_elt: t -> elt
@@ -332,6 +338,7 @@ struct
   let exists f = schema_default true (S.exists f)
   let filter f = schema (fun t -> `Lifted (S.filter f t)) "filter on `Top"
   let elements = schema S.elements "elements on `Top"
+  let to_seq = schema S.to_seq "to_seq on `Top"
   let of_list xs = `Lifted (S.of_list xs)
   let cardinal = schema S.cardinal "cardinal on `Top"
   let min_elt = schema S.min_elt "min_elt on `Top"
@@ -471,6 +478,7 @@ struct
   let mem e e' = E.leq e e'
   let choose e = e
   let elements e = [e]
+  let to_seq e = Seq.return e
   let remove e e' =
     if E.leq e' e then
       E.bot () (* NB! strong removal *)

src/goblint_lib.ml

@@ -128,6 +128,7 @@ module BasePriv = BasePriv
 module RelationPriv = RelationPriv
 module ThreadEscape = ThreadEscape
 module PthreadSignals = PthreadSignals
+module PthreadBarriers = PthreadBarriers
 module ExtractPthread = ExtractPthread
 
 (** {2 Longjmp}

src/util/library/libraryDesc.ml

@@ -69,6 +69,8 @@ type special =
   | SemDestroy of Cil.exp
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
+  | BarrierWait of Cil.exp
+  | BarrierInit of { barrier: Cil.exp; attr:Cil.exp; count: Cil.exp; }
   | Math of { fun_args: math; }
   | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
   | Bzero of { dest: Cil.exp; count: Cil.exp; }

src/util/library/libraryFunctions.ml

@@ -520,6 +520,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
     ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]);
     ("pthread_key_delete", unknown [drop "key" [f]]);
+    ("pthread_barrier_init", special [__ "barrier" []; __ "attr" []; __ "count" []] @@ fun barrier attr count -> BarrierInit {barrier; attr; count});
+    ("pthread_barrier_wait", special [__ "barrier" []] @@ fun barrier -> BarrierWait barrier);
     ("pthread_cancel", unknown [drop "thread" []]);
     ("pthread_testcancel", unknown []);
     ("pthread_setcancelstate", unknown [drop "state" []; drop "oldstate" [w]]);

tests/regression/86-barrier/01-simple.c

@@ -0,0 +1,27 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include<goblint.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
+
+    __goblint_check(i == 0);
+    return 0;
+}