Skip to content

Commit 381e009

Browse files
vesalvojdanivesalvojdani
authored
Merge pull request #5 from goblint/incremental-bench
Incremental benchmarking script and suite
2 parents c31ef82 + 5996535 commit 381e009

40 files changed

+958
-10
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@ bench_result
55
goblint
66
juliet/C
77
juliet/summary_table.html
8+
incremental_data

‎README.md‎

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,23 @@
11
# Goblint benchmark suite
22

3-
[![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)
3+
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.
44

5-
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`).
5+
## Basic Benchmarks
6+
7+
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`).
8+
9+
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.
10+
11+
12+
## Incremental Benchmarks
13+
14+
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...)
15+
2. Run `./update_bench_incremental.rb`
16+
17+
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.
18+
19+
## Other Benchmarking scripts
20+
21+
- [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
22+
- [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
23+
- [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‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{
2+
"ana": {
3+
"int": {
4+
"interval": true
5+
}
6+
}
7+
}

‎index/incremental.txt‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
FromScratch:
2+
Incremental: --disable incremental.reluctant.on
3+
Reluctant: --enable incremental.reluctant.on
4+
5+
6+
Group: POSIX Apps
7+
8+
example
9+
Restarting example
10+
pthread/example.c
11+
-
12+
13+
aget_comb
14+
Multithreaded wget
15+
pthread/aget_comb.c
16+
-
17+
18+
knot_comb
19+
Multithreaded web server
20+
pthread/knot_comb.c
21+
-
22+
23+
ypbind_comb
24+
Linux NIS daemon: ypbind-mt
25+
pthread/ypbind_comb.c
26+
-
27+
28+
smtprc_comb
29+
SMTP Open Relay Checker
30+
pthread/smtprc_comb.c
31+
-

‎index/interactive.txt‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
FromScratch:
2+
Basic: --disable incremental.restart.sided.enabled --disable incremental.reluctant.on
3+
Reluctant: --disable incremental.restart.sided.enabled --enable incremental.reluctant.on
4+
Restart: --enable incremental.restart.sided.enabled --disable incremental.reluctant.on
5+
Both: --enable incremental.restart.sided.enabled --enable incremental.reluctant.on
6+
7+
Group: Our Examples
8+
9+
example
10+
Motivating example
11+
synthetic/incremental/example.c
12+
-
13+
14+
restart
15+
Restarting example
16+
synthetic/incremental/restart.c
17+
-
18+
19+
local-wpoint
20+
Local restart
21+
synthetic/incremental/local-wpoint.c
22+
-
23+
24+
local-wp-read
25+
More difficult local restart
26+
synthetic/incremental/local-wp-read.c
27+
-
28+
29+
justglob
30+
Just check the initial state
31+
synthetic/incremental/justglob.c
32+
-
33+
34+
branch
35+
Change in a condition containing global
36+
synthetic/incremental/branch.c
37+
-
38+
39+
Group: POSIX Apps
40+
41+
aget_comb
42+
Multithreaded wget
43+
pthread/aget_comb.c
44+
-
45+
46+
knot_comb
47+
Multithreaded web server
48+
pthread/knot_comb.c
49+
-
50+
51+
ypbind_comb
52+
Linux NIS daemon: ypbind-mt
53+
pthread/ypbind_comb.c
54+
-
55+
56+
smtprc_comb
57+
SMTP Open Relay Checker
58+
pthread/smtprc_comb.c
59+
-

‎linux/drivers/char/apm-emulation01.patch‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c
2+
index dd9dfa1..324c821 100644
3+
--- linux/drivers/char/apm-emulation.c
4+
+++ linux/drivers/char/apm-emulation.c
5+
@@ -369,11 +369,11 @@ static int apm_open(struct inode * inode, struct file * filp)
6+
* we might close the device immediately without doing a
7+
* privileged operation -- cevans
8+
*/
9+
+ down_write(&user_list_lock);
10+
as->suser = capable(CAP_SYS_ADMIN);
11+
as->writer = (filp->f_mode & FMODE_WRITE) == FMODE_WRITE;
12+
as->reader = (filp->f_mode & FMODE_READ) == FMODE_READ;
13+
14+
- down_write(&user_list_lock);
15+
list_add(&as->list, &apm_user_list);
16+
up_write(&user_list_lock);
17+

‎linux/drivers/char/apm-emulation02.patch‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c
2+
index dd9dfa1..a628a88 100644
3+
--- linux/drivers/char/apm-emulation.c
4+
+++ linux/drivers/char/apm-emulation.c
5+
@@ -320,10 +320,10 @@ apm_ioctl(struct file *filp, u_int cmd, u_long arg)
6+
as->suspend_result = pm_suspend(PM_SUSPEND_MEM);
7+
}
8+
9+
- mutex_lock(&state_lock);
10+
+ //mutex_lock(&state_lock);
11+
err = as->suspend_result;
12+
as->suspend_state = SUSPEND_NONE;
13+
- mutex_unlock(&state_lock);
14+
+ //mutex_unlock(&state_lock);
15+
break;
16+
}
17+

‎linux/drivers/char/apm-emulation03.patch‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c
2+
index dd9dfa1..f89b8dd 100644
3+
--- linux/drivers/char/apm-emulation.c
4+
+++ linux/drivers/char/apm-emulation.c
5+
@@ -210,7 +210,7 @@ static ssize_t apm_read(struct file *fp, char __user *buf, size_t count, loff_t
6+
{
7+
struct apm_user *as = fp->private_data;
8+
apm_event_t event;
9+
- int i = count, ret = 0;
10+
+ int i = count, ret = 1;
11+
12+
if (count < sizeof(apm_event_t))
13+
return -EINVAL;

‎linux/drivers/char/applicom01.patch‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
174c174
2+
< for (i = 0; i < MAX_BOARD; i++) {
3+
---
4+
> for (i = 0; i <= MAX_BOARD; i++) {

‎linux/drivers/char/bsr01.patch‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
diff --git linux/drivers/char/bsr.c linux/drivers/char/bsr.c
2+
index a6cef54..6c6efe2 100644
3+
--- linux/drivers/char/bsr.c
4+
+++ linux/drivers/char/bsr.c
5+
@@ -284,7 +284,7 @@ static int bsr_add_node(struct device_node *bn)
6+
7+
static int bsr_create_devs(struct device_node *bn)
8+
{
9+
- int ret;
10+
+ int ret = -1;
11+
12+
while (bn) {
13+
ret = bsr_add_node(bn);

0 commit comments

Comments
 (0)