Merge pull request #1399 from goblint/lockcentered_tid

Ego-Lane-Derived-Digests for Privatizations: `Lock- ` & `Write-Centered` Privatizations

src/config/options.schema.json

@@ -752,9 +752,9 @@
             "privatization": {
               "title": "ana.base.privatization",
               "description":
-                "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock",
+                "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid",
               "type": "string",
-              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"],
               "default": "protection-read"
             },
             "priv": {

tests/regression/13-privatized/18-first-reads.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.int.interval true
+// PARAM: --set ana.int.interval true --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>

tests/regression/13-privatized/53-pfscan_widen_dependent_minimal.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval --enable exp.priv-distr-init --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>

tests/regression/13-privatized/55-widen-dependent-local.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval --enable exp.priv-distr-init  --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>

tests/regression/13-privatized/77-lock-tid.c

@@ -0,0 +1,48 @@
+// PARAM: --set ana.base.privatization lock-tid --enable ana.int.interval --set ana.path_sens[+] mutex
+// Based on the example {e:lock-centered-beats-write-centered} from the draft of Michael Schwarz's PhD thesis.
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t a;
+pthread_mutex_t d;
+
+
+void* other()
+{
+  pthread_mutex_lock(&d);
+  pthread_mutex_lock(&a);
+  g = 42;
+  pthread_mutex_unlock(&a);
+  g = 17;
+  pthread_mutex_unlock(&d);
+  return 0;
+}
+
+void* there_i_ruined_it()
+{
+  pthread_mutex_lock(&a);
+  g = 45;
+  pthread_mutex_unlock(&a);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  pthread_t tid1;
+  pthread_t tid2;
+  pthread_create(&tid1, 0, other, 0);
+
+  pthread_mutex_lock(&d);
+  pthread_mutex_lock(&a);
+  pthread_mutex_unlock(&d);
+
+  x = g;
+  // Succeeds with lock, fails with write
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(x <= 17);
+
+  pthread_create(&tid2, 0, there_i_ruined_it, 0);
+  return 0;
+}

tests/regression/13-privatized/78-write-tid.c

@@ -0,0 +1,67 @@
+// PARAM: --set ana.base.privatization write-tid --enable ana.int.interval --set ana.path_sens[+] mutex
+// Based on the example {e:write-centered} from the draft of Michael Schwarz's PhD thesis.
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t a;
+pthread_mutex_t b;
+pthread_mutex_t c;
+
+
+void* t1()
+{
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+  g = 42;
+  pthread_mutex_unlock(&a);
+  g = 17;
+  pthread_mutex_unlock(&b);
+}
+
+void* t2()
+{
+  pthread_mutex_lock(&c);
+  g = 59;
+  pthread_mutex_unlock(&c);
+  return 0;
+}
+
+void* there_i_ruined_it()
+{
+  pthread_mutex_lock(&a);
+  g = 45;
+  pthread_mutex_unlock(&a);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  pthread_t tid1;
+  pthread_t tid2;
+  pthread_t tid3;
+
+  pthread_create(&tid1, 0, t1, 0);
+  pthread_create(&tid2, 0, t2, 0);
+
+  pthread_mutex_lock(&c);
+  g=31;
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+
+  x = g;
+
+  // Succeed with write & lock
+  __goblint_check(x >= 17);
+
+  // Succeeds with write-tid & lock-tid
+  __goblint_check(x <= 42);
+
+  // Succeeds with write, fails with lock
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(x <= 31);
+
+  pthread_create(&tid3, 0, there_i_ruined_it, 0);
+  return 0;
+}

tests/regression/13-privatized/79-write-lock-tid.c

@@ -0,0 +1,91 @@
+// PARAM: --set ana.base.privatization write+lock-tid --enable ana.int.interval --set ana.path_sens[+] mutex
+// Based on combining the examples {e:lock-centered-beats-write-centered} and {e:write-centered} from the draft of Michael Schwarz's PhD thesis.
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t a;
+pthread_mutex_t b;
+pthread_mutex_t c;
+
+int xg;
+pthread_mutex_t xa;
+pthread_mutex_t xd;
+
+
+void* t1()
+{
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+  g = 42;
+  pthread_mutex_unlock(&a);
+  g = 17;
+  pthread_mutex_unlock(&b);
+
+  pthread_mutex_lock(&xd);
+  pthread_mutex_lock(&xa);
+  xg = 42;
+  pthread_mutex_unlock(&xa);
+  xg = 17;
+  pthread_mutex_unlock(&xd);
+}
+
+void* t2()
+{
+  pthread_mutex_lock(&c);
+  g = 59;
+  pthread_mutex_unlock(&c);
+  return 0;
+}
+
+void* there_i_ruined_it()
+{
+  pthread_mutex_lock(&a);
+  g = 45;
+  pthread_mutex_unlock(&a);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  int xx;
+  pthread_t tid1;
+  pthread_t tid2;
+  pthread_t tid3;
+
+  pthread_create(&tid1, 0, t1, 0);
+  pthread_create(&tid2, 0, t2, 0);
+
+  pthread_mutex_lock(&c);
+  g=31;
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+
+  x = g;
+
+  // Succeed with write & lock
+  __goblint_check(x >= 17);
+
+  // Succeeds with write-tid & lock-tid
+  __goblint_check(x <= 42);
+
+  // Succeeds with write, fails with lock
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(x <= 31);
+
+
+  pthread_mutex_lock(&xd);
+  pthread_mutex_lock(&xa);
+  pthread_mutex_unlock(&xd);
+
+  xx = xg;
+  // Succeeds with lock, fails with write
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(xx <= 17);
+
+
+
+  pthread_create(&tid3, 0, there_i_ruined_it, 0);
+  return 0;
+}

tests/regression/66-interval-set-one/62-pfscan_widen_dependent_minimal.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>

tests/regression/66-interval-set-one/98-widen-dependent-local.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>

tests/regression/67-interval-sets-two/43-first-reads.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.int.interval_set true
+// PARAM: --set ana.int.interval_set true --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>