polyvios / locksmith Goto Github PK

Dear Polyvios,
Hello, sorry to bother you. I want try LockSmith to detect data race, but i have trouble in installation.
I have installed Ocaml 4.05 CIL 0.07 and Banshee, but when I run ./configure ,
at the end it shows like this:

config.status: config.h is unchanged
CIL configuration:
architecture/OS: ARCHOS x86_LINUX
source tree root: CILHOME /home/haining/data-race-tool/locksmith-1.0/cil
(optional) cl.exe found: HAS_MSVC no
gcc to use CC gcc
default compiler DEFAULT_COMPILER _GNUCC
CIL version CIL_VERSION 1.3.7
CIL features CIL_FEATURES locksmith lockpick stmizer
Extra source directories EXTRASRCDIRS /home/haining/data-race-tool/locksmith-1.0/src
Cycles per microsecond CYCLES_PER_USEC 0
sed: -e expression #1, char 49: number option to s' command may not be zero sed: -e expression #1, char 49: number option to s' command may not be zero

And when I run make, it shows:

make[1]: Entering directory '/home/haining/data-race-tool/locksmith-1.0/banshee'
make -C libcompat
make[2]: Entering directory '/home/haining/data-race-tool/locksmith-1.0/banshee/libcompat'
cc -c -Wall -Ddeletes="" -DNMEMDEBUG -DNDEBUG -Werror -fno-common -o regions.o regions.c
In file included from regions.c:111:0:
pages.c: In function ‘set_region_range’:
pages.c:332:3: error: this ‘while’ clause does not guard... [-Werror=misleading-indentation]
while (firstm < lastm || firstp <= lastp)
^~~~~
pages.c:337:5: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the ‘while’
set_page_region(firstm, firstp++, r);
^~~~~~~~~~~~~~~
cc1: all warnings being treated as errors
Makefile:43: recipe for target 'regions.o' failed
make[2]: *** [regions.o] Error 1
make[2]: Leaving directory '/home/haining/data-race-tool/locksmith-1.0/banshee/libcompat'
Makefile:41: recipe for target 'libcompat' failed
make[1]: *** [libcompat] Error 2
make[1]: Leaving directory '/home/haining/data-race-tool/locksmith-1.0/banshee'
Makefile:47: recipe for target 'all' failed
make: *** [all] Error 2

The tool is excellent, and I really want to have a try, Can you help me see what went wrong?
I'd appreciate it greatly if you can give me some guides.

Best,
Haining

Overall, locksmith works very well as a verification tool: there are only two unsoundness issues. The first is just because locksmith does not register accesses on arguments to scanf. Since locksmith warns that this is an unknown function, I made locksmith answer "unknown" in this case, so this is not counted as a wrong verdict.

The only real unsoundness issue occurs on a benchmark where two distinct mutexes are chosen non-deterministically. One can simplify the issue to the following example, which has no branching:

#include <pthread.h>

int myglobal;
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
  pthread_mutex_lock(&mutex1);
  myglobal=myglobal+1;
  pthread_mutex_unlock(&mutex1);
  return NULL;
}

int main(void) {
  pthread_t id;
  pthread_mutex_t *m;

  m = &mutex1;
  m = &mutex2;

  pthread_create(&id, NULL, t_fun, NULL);

  pthread_mutex_lock(m);
  myglobal=myglobal+1;
  pthread_mutex_unlock(m);

  pthread_join (id, NULL);
  return 0;
}

Locksmith does not complain about the above program in its default configuration and I tried various flow-sensitivity options, but the result is still the same. It is as if both mutex1 and mutex2 is seen to be flowing to m. I wonder if there is some flag that I'm overlooking here or is it a real bug?

I compiled locksmith on a fresh installation of Ubuntu 20.04 as suggested:

sudo apt install gcc opam autoconf automake make gperf python indent emacs flex bison
git submodule update --init --recursive
opam init -n
opam switch create . 3.11.2
eval $(opam env)
./configure
make

But I got the following error:

make[1]: Entering directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee'
make -C libcompat
make[2]: Entering directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee/libcompat'
make[2]: Nothing to be done for 'all'.
make[2]: Leaving directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee/libcompat'
make -C codegen
make[2]: Entering directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee/codegen'
make[3]: Entering directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee/codegen'
ocamlc -c spec_to_c.ml
File "spec_to_c.ml", line 129, characters 17-39:
Error: Unbound value String.uppercase_ascii
make[3]: *** [OcamlMakefile:868: spec_to_c.cmo] Error 2
make[3]: Leaving directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee/codegen'
make[2]: *** [OcamlMakefile:630: byte-code] Error 2
make[2]: Leaving directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee/codegen'
make[1]: *** [Makefile:47: codegen] Error 2
make[1]: Leaving directory '/home/ubuntu/Downloads/GitHub/locksmith/banshee'
make: *** [Makefile:47: all] Error 2

I am not familiar with Ocaml and do not know how to solve this problem.
Any feedback will be appreciate!