Incremental benchmarking script and suite

.gitignore

@@ -5,3 +5,4 @@ bench_result
 goblint
 juliet/C
 juliet/summary_table.html
+incremental_data

README.md

@@ -1,5 +1,23 @@
 # Goblint benchmark suite
 
-[![Gitter](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/goblint/bench?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
+This contains the suite of benchmarks we currently use to evaluate Goblint. To run the benchmarks, make sure this repository is checked out in a directory with the same parent as the Goblint analyzer. 
 
-This contains the suite of benchmarks we currently use to evaluate Goblint. To run the benchmarks, make sure this repository is checked out in a directory with the same parent as the Goblint analyzer. Then, you can execute the script `./update_bench.rb` and view the results in bench_result/index.html. The kernel benchmarks rely on linux headers in the analyzer's directory (installed by executing `make headers`).
+## Basic Benchmarks
+
+Execute the script `./update_bench.rb` and view the results in bench_result/index.html. The kernel benchmarks rely on linux headers in the analyzer's directory (installed by executing `make headers`). 
+
+The benchmarks descriptions are assumed to be in a file called `bench.txt`. If this is absent it is symlinked to `index/dd.txt`. The idea was that one should locally replace with a hard copy without modifying the default descriptions. 
+
+
+## Incremental Benchmarks
+
+1. Edit the file `index/incremental.txt` to set the parameters. Do not add the incremental save and load commands since these are added by some ugly mechanism. (Be happy I'm keeping my hands away from goblint...)
+2. Run `./update_bench_incremental.rb`
+
+Add patches by changing some benchmark and doing, e.g., `git diff --no-prefix dtlk.c > dtlk04.patch`, and then of course restore the file. 
+
+## Other Benchmarking scripts
+
+- [parallel-run.sh](https://github.com/goblint/bench/blob/2d8bc2c8cb2cd6499733c535b868643f45bcae49/parallel-run.sh) to run the config in that script in parallel and log each program
+- [csv-results.ml](https://github.com/goblint/bench/blob/2d8bc2c8cb2cd6499733c535b868643f45bcae49/csv-results.ml) to extract some numbers from each log and print a csv of it
+- [precision.sh](https://github.com/goblint/bench/blob/2d8bc2c8cb2cd6499733c535b868643f45bcae49/precision.sh) to let goblint compare two variants for each program and write the result to a .precision file

index/incremental.json

@@ -0,0 +1,7 @@
+{
+      "ana": {
+        "int": {
+            "interval": true
+        }
+    }
+}

index/incremental.txt

@@ -0,0 +1,31 @@
+FromScratch: 
+Incremental: --disable incremental.reluctant.on
+Reluctant: --enable incremental.reluctant.on
+
+
+Group: POSIX Apps
+
+example
+Restarting example
+pthread/example.c
+-
+
+aget_comb
+Multithreaded wget
+pthread/aget_comb.c
+-
+
+knot_comb
+Multithreaded web server
+pthread/knot_comb.c
+-
+
+ypbind_comb
+Linux NIS daemon: ypbind-mt
+pthread/ypbind_comb.c
+-
+
+smtprc_comb
+SMTP Open Relay Checker
+pthread/smtprc_comb.c
+-

index/interactive.txt

@@ -0,0 +1,52 @@
+FromScratch:
+Incremental: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on
+Reluctant: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on
+RestartGlob: --enable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on
+RestartLocal: --enable incremental.restart.sided.enabled --enable incremental.restart.wpoint.enabled --disable incremental.reluctant.on
+
+
+Group: Our Examples
+
+example
+Motivating example
+synthetic/incremental/example.c
+-
+
+restart
+Restarting example
+synthetic/incremental/restart.c
+-
+
+local-wpoint
+Local restart
+synthetic/incremental/local-wpoint.c
+-
+
+local-wp-read
+More difficult local restart
+synthetic/incremental/local-wp-read.c
+-
+
+
+
+Group: POSIX Apps
+
+aget_comb
+Multithreaded wget
+pthread/aget_comb.c
+-
+
+knot_comb
+Multithreaded web server
+pthread/knot_comb.c
+-
+
+ypbind_comb
+Linux NIS daemon: ypbind-mt
+pthread/ypbind_comb.c
+-
+
+smtprc_comb
+SMTP Open Relay Checker
+pthread/smtprc_comb.c
+-

linux/drivers/char/apm-emulation01.patch

@@ -0,0 +1,17 @@
+diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c
+index dd9dfa1..324c821 100644
+--- linux/drivers/char/apm-emulation.c
++++ linux/drivers/char/apm-emulation.c
+@@ -369,11 +369,11 @@ static int apm_open(struct inode * inode, struct file * filp)
+ 		 * we might close the device immediately without doing a
+ 		 * privileged operation -- cevans
+ 		 */
++		down_write(&user_list_lock);
+ 		as->suser = capable(CAP_SYS_ADMIN);
+ 		as->writer = (filp->f_mode & FMODE_WRITE) == FMODE_WRITE;
+ 		as->reader = (filp->f_mode & FMODE_READ) == FMODE_READ;
+
+-		down_write(&user_list_lock);
+ 		list_add(&as->list, &apm_user_list);
+ 		up_write(&user_list_lock);
+

linux/drivers/char/apm-emulation02.patch

@@ -0,0 +1,17 @@
+diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c
+index dd9dfa1..a628a88 100644
+--- linux/drivers/char/apm-emulation.c
++++ linux/drivers/char/apm-emulation.c
+@@ -320,10 +320,10 @@ apm_ioctl(struct file *filp, u_int cmd, u_long arg)
+ 			as->suspend_result = pm_suspend(PM_SUSPEND_MEM);
+ 		}
+
+-		mutex_lock(&state_lock);
++		//mutex_lock(&state_lock);
+ 		err = as->suspend_result;
+ 		as->suspend_state = SUSPEND_NONE;
+-		mutex_unlock(&state_lock);
++		//mutex_unlock(&state_lock);
+ 		break;
+ 	}
+

linux/drivers/char/apm-emulation03.patch

@@ -0,0 +1,13 @@
+diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c
+index dd9dfa1..f89b8dd 100644
+--- linux/drivers/char/apm-emulation.c
++++ linux/drivers/char/apm-emulation.c
+@@ -210,7 +210,7 @@ static ssize_t apm_read(struct file *fp, char __user *buf, size_t count, loff_t
+ {
+ 	struct apm_user *as = fp->private_data;
+ 	apm_event_t event;
+-	int i = count, ret = 0;
++	int i = count, ret = 1;
+
+ 	if (count < sizeof(apm_event_t))
+ 		return -EINVAL;

linux/drivers/char/applicom01.patch

@@ -0,0 +1,4 @@
+174c174
+< 	for (i = 0; i < MAX_BOARD; i++) {
+---
+> 	for (i = 0; i <= MAX_BOARD; i++) {

linux/drivers/char/bsr01.patch

@@ -0,0 +1,13 @@
+diff --git linux/drivers/char/bsr.c linux/drivers/char/bsr.c
+index a6cef54..6c6efe2 100644
+--- linux/drivers/char/bsr.c
++++ linux/drivers/char/bsr.c
+@@ -284,7 +284,7 @@ static int bsr_add_node(struct device_node *bn)
+
+ static int bsr_create_devs(struct device_node *bn)
+ {
+-	int ret;
++	int ret = -1;
+
+ 	while (bn) {
+ 		ret = bsr_add_node(bn);

linux/drivers/char/dtlk01.patch

@@ -0,0 +1,13 @@
+diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c
+index 65a8d96..86157f6 100644
+--- linux/drivers/char/dtlk.c
++++ linux/drivers/char/dtlk.c
+@@ -215,7 +215,7 @@ static ssize_t dtlk_write(struct file *file, const char __user *buf,
+
+ 		msleep_interruptible(1);
+
+-		if (++retries > 10 * HZ) { /* wait no more than 10 sec
++		if (++retries > 12 * HZ) { /* wait no more than 10 sec
+ 					      from last write */
+ 			printk("dtlk: write timeout.  "
+ 			       "inb_p(dtlk_port_tts) = 0x%02x\n",

linux/drivers/char/dtlk02.patch

@@ -0,0 +1,12 @@
+diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c
+index 65a8d96..9257c7d 100644
+--- linux/drivers/char/dtlk.c
++++ linux/drivers/char/dtlk.c
+@@ -261,7 +261,7 @@ static unsigned int dtlk_poll(struct file *file, poll_table * wait)
+
+ static void dtlk_timer_tick(unsigned long data)
+ {
+-	TRACE_TEXT(" dtlk_timer_tick");
++	TRACE_TEXT(" dtlk_timer_tick_tock");
+ 	wake_up_interruptible(&dtlk_process_list);
+ }

linux/drivers/char/dtlk03.patch

@@ -0,0 +1,16 @@
+diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c
+index 65a8d96..4a5499e 100644
+--- linux/drivers/char/dtlk.c
++++ linux/drivers/char/dtlk.c
+@@ -277,9 +277,9 @@ static long dtlk_ioctl(struct file *file,
+ 	switch (cmd) {
+
+ 	case DTLK_INTERROGATE:
+-		mutex_lock(&dtlk_mutex);
++		//mutex_lock(&dtlk_mutex);
+ 		sp = dtlk_interrogate();
+-		mutex_unlock(&dtlk_mutex);
++		//mutex_unlock(&dtlk_mutex);
+ 		if (copy_to_user(argp, sp, sizeof(struct dtlk_settings)))
+ 			return -EINVAL;
+ 		return 0;

linux/drivers/char/dtlk04.patch

@@ -0,0 +1,13 @@
+diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c
+index 65a8d96..deff366 100644
+--- linux/drivers/char/dtlk.c
++++ linux/drivers/char/dtlk.c
+@@ -302,7 +302,7 @@ static int dtlk_open(struct inode *inode, struct file *file)
+ 	switch (iminor(inode)) {
+ 	case DTLK_MINOR:
+ 		if (dtlk_busy)
+-			return -EBUSY;
++			return -EPIPE;
+ 		return nonseekable_open(inode, file);
+
+ 	default:

pthread/aget_comb01.patch

@@ -0,0 +1,14 @@
+diff --git pthread/aget_comb.c pthread/aget_comb.c
+index c7d24b4..d505c6e 100644
+--- pthread/aget_comb.c
++++ pthread/aget_comb.c
+@@ -1017,7 +1017,8 @@ void *signal_waiter(void *arg )
+   while (1) {
+     sigwait((sigset_t const   * __restrict  )(& signal_set), (int * __restrict  )(& signal___0));
+     switch (signal___0) {
+-    case 2: 
++    case 2:
++    case 3:
+     sigint_handler();
+     break;
+     case 14: 

pthread/aget_comb02.patch

@@ -0,0 +1,13 @@
+diff --git pthread/aget_comb.c pthread/aget_comb.c
+index c7d24b4..bd0a90a 100644
+--- pthread/aget_comb.c
++++ pthread/aget_comb.c
+@@ -1094,7 +1094,7 @@ void *http_get(void *arg )
+   tmp = calloc(8192U, sizeof(char ));
+   rbuf = (char *)tmp;
+   sd = socket(2, 1, 0);
+-  if (sd == -1) {
++  if (sd <= -1) {
+     tmp___0 = __errno_location();
+     tmp___1 = strerror(*tmp___0);
+     Log((char *)"<THREAD #%ld> socket creation failed: %s", tid, tmp___1);

pthread/example.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <pthread.h>
+
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+int (*fp)() = NULL;
+
+int bad() {
+    return -1;
+}
+
+int good() {
+    return 1;
+}
+
+void* consumer(void *arg) {
+    int res = 0;
+    pthread_mutex_lock(&mutex);
+    if (fp != NULL) {
+        res = fp();
+    }
+    pthread_mutex_unlock(&mutex);
+    assert(res >= 0);
+    res = 0;
+    // change absorbed
+    return NULL;
+}
+
+void* producer(void *arg) {
+    int res = 0;
+    pthread_mutex_lock(&mutex);
+    fp = bad;
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+int main() {
+    pthread_t id1 = NULL, id2 = NULL;
+    pthread_create(&id1, NULL, consumer, NULL);
+    pthread_create(&id2, NULL, producer, NULL);
+    return 0;
+}

pthread/example01.patch

@@ -0,0 +1,4 @@
+32c32
+<     fp = bad;
+---
+>     fp = good;

pthread/knot_comb01.patch

@@ -0,0 +1,13 @@
+diff --git pthread/knot_comb.c pthread/knot_comb.c
+index ad59515..1a65063 100644
+--- pthread/knot_comb.c
++++ pthread/knot_comb.c
+@@ -1106,7 +1106,7 @@ void accept_loop(int id , int s )
+       if (! attr_init_done) {
+         pthread_attr_init(& attr);
+         rv = pthread_attr_setdetachstate(& attr, 1);
+-        if (! (rv == 0)) {
++        if (rv != 0) {
+           assert_failed((char *)"knot.c", 472U, "accept_loop", (char *)"rv == 0");
+         }
+         attr_init_done = 1;

pthread/knot_comb02.patch

@@ -0,0 +1,13 @@
+diff --git pthread/knot_comb.c pthread/knot_comb.c
+index ad59515..de401be 100644
+--- pthread/knot_comb.c
++++ pthread/knot_comb.c
+@@ -709,7 +709,7 @@ char *input_get_line(input_state *state )
+         empty = & state->buf[state->valid];
+         tmp = read(state->socket, (void *)empty, (unsigned int )(511 - state->valid));
+         n = tmp;
+-        if (n <= 0) {
++        if (n == 0) {
+           result = (char *)((void *)0);
+           done = 1;
+         } else {

pthread/smtprc_comb01.patch

@@ -0,0 +1,13 @@
+diff --git pthread/smtprc_comb.c pthread/smtprc_comb.c
+index 8aaffec..7c8c514 100644
+--- pthread/smtprc_comb.c
++++ pthread/smtprc_comb.c
+@@ -3789,7 +3789,7 @@ void print_link(FILE *fd , char *link___0 , char *text , char *color )
+   {
+   x = 0;
+   while (1) {
+-    if (x < 20) {
++    if (x < 16) {
+       tmp = strlen((char const   *)text);
+       if (! ((size_t )x < tmp)) {
+         break;

pthread/smtprc_comb02.patch

@@ -0,0 +1,13 @@
+diff --git pthread/smtprc_comb.c pthread/smtprc_comb.c
+index 8aaffec..6e4480a 100644
+--- pthread/smtprc_comb.c
++++ pthread/smtprc_comb.c
+@@ -4150,7 +4150,7 @@ int relay_check(int *sockfd , long cur_host )
+       strncat((char * __restrict  )(checking), (char const   * __restrict  )" !",
+               8192U);
+       printf((char const   * __restrict  )"%s\n", checking);
+-      return (-1);
++      return (-2);
+     }
+     rule___0 ++;
+   }

pthread/ypbind_comb01.patch

@@ -0,0 +1,13 @@
+diff --git pthread/ypbind_comb.c pthread/ypbind_comb.c
+index 255923b..444fe25 100644
+--- pthread/ypbind_comb.c
++++ pthread/ypbind_comb.c
+@@ -4583,7 +4583,7 @@ int pthread_rdwr_wunlock_np(pthread_rdwr_t *rdwrp ) ;
+ #line 84 "serv_list.c"
+ static struct binding *domainlist  =    (struct binding *)((void *)0);
+ #line 85 "serv_list.c"
+-static int max_domains  =    0;
++static int max_domains  =    4;
+ #line 86 "serv_list.c"
+ static struct __anonstruct_pthread_rdwr_t_72 domainlock  =    {0, 0, 0, {{0, 0U, 0, 0, 0U, {0}}}, {{0, 0U, 0ULL, 0ULL, 0ULL, (void *)0, 0U, 0U}}};
+ #line 87 "serv_list.c"