Add concurrency examples to regression tests #5521

thomasspriggs · 2020-10-09T11:16:15Z

This PR adds concurrency examples to the regression tests in preparation for the planned sequentialization work.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2020-10-09T13:16:30Z

Codecov Report

Merging #5521 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5521   +/-   ##
========================================
  Coverage    68.52%   68.52%           
========================================
  Files         1187     1187           
  Lines        98265    98265           
========================================
  Hits         67339    67339           
  Misses       30926    30926

Flag	Coverage Δ
#cproversmt2	`42.96% <ø> (ø)`
#regression	`65.68% <ø> (ø)`
#unit	`32.26% <ø> (ø)`

Flags with carried forward coverage won't be shown. Click here to find out more.

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1c4e0c4...52c0a80. Read the comment docs.

piotr-grabalski

Lots of code but it looks good to me,

Personally I am not a big fan of including *.c files though ;)

hannes-steffenhagen-diffblue · 2020-10-14T10:09:07Z

regression/cbmc-sequentialization/CMakeLists.txt

@@ -0,0 +1,29 @@
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  set(gcc_only "-X gcc-only")


No quotes, this is the same bug fotis was struggling on windows with :)

If you add quotes here this'll be passed as a single argument to test.pl, i.e. test.pl "-X gcc only" vs test.pl -X gcc-only.

Should be fixed now.

Actually none of this is going to work on Windows as-is, because pthreads isn't natively supported on that platform. I'll either need to disable all these tests, or add a windows test-time dependency for a suitable compatibility layer.

hannes-steffenhagen-diffblue · 2020-10-14T10:10:13Z

regression/cbmc-sequentialization/CMakeLists.txt

+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo ${gcc_only}"


This gcc_only needs to be in the next line, its an argument to test.pl not cbmc.

Should be fixed now.

hannes-steffenhagen-diffblue · 2020-10-14T10:10:52Z

regression/cbmc-sequentialization/CMakeLists.txt

+
+add_test_pl_profile(
+    "cbmc-cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2 ${gcc_only}"


Should be fixed now.

NlightNFotis

Can we get changes on the CMakeLists.txt. I think they are correctness related and pretty important.

regression/cbmc-sequentialization/CMakeLists.txt

martin-cs

Seems good. Thanks for adding the tests first. Will you have these run with and without the sequentialisation? Also, I take it whoever is doing the sequentialisation is aware of the considerable amount of literature on "seqeuntialise and then run CBMC"?

martin-cs · 2020-10-12T11:11:14Z

regression/cbmc-sequentialization/posix_semaphores/blocking_queue.c

+  enqueue(&input_queue, 8);
+  enqueue(&input_queue, 9);
+  enqueue(&input_queue, 0);
+  join_thread(worker_thread1);


I like this example and it should sequentialize well.

martin-cs · 2020-10-12T11:14:08Z

regression/cbmc-sequentialization/pthread_mutex/no_mutex.c

+  for(int i = 0; i < 100; ++i)
+  {
+    int shared_count_copy = shared_count;
+    // The following call to yield is here in order to cause a thread swap


The wording of this sounds a bit certain. I can believe that 99.99% of the time it does but I don't think it is certain to do so.

I would feel better if the comment was reworded so that it captured this kind of "likely but not certain" but it is not a blocking issue.

That'd make more sense to me as well, practically this should work but IMHO it’s probably not a good idea to be overly reliant on specific thread scheduling behaviour.

I have reworded these comments slightly.

martin-cs · 2020-10-12T11:14:29Z

regression/cbmc-sequentialization/pthread_mutex/with_mutex.c

+    const int lock_error = pthread_mutex_lock(&mutex);
+    assert(!lock_error);
+    int shared_count_copy = shared_count;
+    // The following call to yield is here in order to cause a thread swap


NlightNFotis

Thanks for the changes. LGTM! 🎉

thomasspriggs · 2020-10-15T16:48:46Z

Seems good. Thanks for adding the tests first. Will you have these run with and without the sequentialisation? Also, I take it whoever is doing the sequentialisation is aware of the considerable amount of literature on "seqeuntialise and then run CBMC"?

We have been looking into the existing literature and implementations. My thought is to run these specific tests with sequentialisation only, once it is implemented. This is because these test run up against existing limitations without the sequentialisation step. My thought is that the new workflow will look something like -

Run goto-cc on the source.
Run goto-sequentialise on the goto-binary.
Run CBMC against the sequentialised goto-binary.

Therefore this directory will need some kind of chain script, once goto-sequentialise exists. Presuming that we keep the sequentialisation in a separate binary.

martin-cs · 2020-10-15T19:50:49Z

@thomasspriggs : Some thoughts

Last I looked CSeq and Yogar-CBMC were the best sequentialisation tools.
goto-instrument already has some concurrent instrumentation (for weak memory), so you could add it there if you want it to implement it as part of a pipeline.
Most of the sequentialisations I have seen have been underapproximate and slowly increasing the number of interleavings, thread interactions, etc. It feels like it should even be possible to use the SAT model to tell you where needs more freedom (as with BMC and finding which loops need more unwinding). As such, you may want to do multiple sequentialisations and have the parameters of the later ones depend on the output of the earlier ones. If so, do you want to do that with multiple program calls and a script or have one program?

HTH

hannes-steffenhagen-diffblue

Not done reviewing yet just to get these out of the way:

hannes-steffenhagen-diffblue · 2020-10-15T09:25:09Z

regression/cbmc-sequentialization/pthread_cond/test.c

+}
+
+// Wait for signal. Note that pthreads requires us to lock and unlock the mutex
+// around the call to `pthread_cond_wait`.


Maybe worth pointing out if you want to clarify behavior unfamiliar with pthreads that in the period between calling pthread_cond_wait and it returning the mutex is actually unlocked, just in case anyone is wondering if this doesn't block everything else.

hannes-steffenhagen-diffblue · 2020-10-15T09:26:27Z

regression/cbmc-sequentialization/pthread_cond/test.c

+{
+  const int lock_error = pthread_mutex_lock(&signal_mutex);
+  assert(!lock_error);
+  const int wait_error = pthread_cond_wait(&condition, &signal_mutex);


Writing these comments as I go – note that POSIX requires an associated boolean condition with the condition variable, and correct wake-up behaviour should always be a loop that's waiting and checking the condition after the wait call. Even if the condition you want to wait on is just "someone called signal() at some point" this does, at minimum, still require a flag to operate correctly.

When using condition variables there is always a Boolean predicate involving shared variables associated with each condition wait that is true if the thread should proceed. Spurious wakeups from the pthread_cond_timedwait() or pthread_cond_wait() functions may occur. Since the return from pthread_cond_timedwait() or pthread_cond_wait() does not imply anything about the value of this predicate, the predicate should be re-evaluated upon such return.

Without this the expected result for this benchmark should actually be a failure, as a spurious wakeup is possible (this also means that actually we literally don't need to do anything to model signal and wait correctly other than unlocking and then locking the mutex...). Which to be clear isn't a bad thing, "there is a bug here and we can find it" is a more interesting result (and therefore test) than "we can't find anything here", but this should be documented as such so a future developer doesn't scratch their head why this test is failing despite everything seemingly working as intended.

hannes-steffenhagen-diffblue · 2020-10-15T09:39:13Z

regression/cbmc-sequentialization/pthread_mutex/no_mutex.c

+  for(int i = 0; i < 100; ++i)
+  {
+    int shared_count_copy = shared_count;
+    // The following call to yield is here in order to cause a thread swap


That'd make more sense to me as well, practically this should work but IMHO it’s probably not a good idea to be overly reliant on specific thread scheduling behaviour.

hannes-steffenhagen-diffblue · 2020-10-15T09:42:53Z

regression/cbmc-sequentialization/pthread_mutex/no_mutex.c

+{
+  for(int i = 0; i < 100; ++i)
+  {
+    int shared_count_copy = shared_count;


might be worth pointing out here that the odd construction with the copy-then-increment is because our intended approach (sequentialisation) will give us sequential consistency at the statement level, so an increment operation is going to be atomic for us.

hannes-steffenhagen-diffblue

Couple nitpicks here and there, nothing blocking I think.

hannes-steffenhagen-diffblue · 2020-10-19T10:49:12Z

regression/cbmc-sequentialization/posix_semaphores/util.c

@@ -0,0 +1,33 @@
+


I do have to agree the util.c is slightly sketchy, generally I prefer if tests stay self contained, even if that means duplicating some code. If you think it's worth it to give more emphasis to the parts that are actually different between tests we can leave it as is though.

I have removed util.c and duplicated the code. I instinctively dislike cut and pasting code. But I am willing to accept that different ways of doing things may be better for test code.

hannes-steffenhagen-diffblue · 2020-10-19T11:01:15Z

regression/cbmc-sequentialization/posix_semaphores/create_destroy.c

+
+sem_t global_semaphore;
+
+void *worker(void *arguments)


⛏️ Unused function?

hannes-steffenhagen-diffblue · 2020-10-19T11:03:00Z

regression/cbmc-sequentialization/posix_semaphores/util.c

+  const pthread_attr_t *const attributes = NULL;
+  void *const worker_argument = NULL;
+  const int create_status =
+    pthread_create(&worker_thread, attributes, &worker, worker_argument);


I really don’t like that this assumes the existence of a function with exactly this name, what's wrong with passing this in as an argument?

I have now fixed this for the semaphores examples.

hannes-steffenhagen-diffblue · 2020-10-19T11:07:01Z

regression/cbmc-sequentialization/posix_semaphores/blocking_queue.c

+    "enqueue begin:%lu end:%lu data:%d \n", queue->begin, queue->end, data);
+  const int free_wait_error = sem_wait(&queue->free_space);
+  assert(free_wait_error == false);
+  queue->elements[queue->end] = data;


❓

Is the intention here that enqueue and dequeue are only allowed to be called from one thread respectively? Otherwise this would be a data race. If so, can you document this here?

Yes. This queue implementation is only safe with a single enqueuing and dequeuing thread. I will add some comments to detail this limitation.

hannes-steffenhagen-diffblue · 2020-10-19T11:07:56Z

regression/cbmc-sequentialization/rw_lock/race_test.c

@@ -0,0 +1,2 @@
+#define NO_LOCKS


Again, I don't like having tests split up over multiple files like this too much if we don't have to..

Ok. I have pushed a commit which duplicates this instead.

hannes-steffenhagen-diffblue · 2020-10-19T11:09:17Z

regression/cbmc-sequentialization/rw_lock/with_lock.c

+  struct sharedt *shared = (struct sharedt *)arguments;
+  for(int i = 0; i < 1000; ++i)
+  {
+#ifndef NO_LOCKS


I think these would be easier to follow if you had just copy&pasted the code.

hannes-steffenhagen-diffblue · 2020-10-19T12:25:52Z

regression/cbmc-sequentialization/posix_semaphores/blocking_wait.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers


I'd be careful with naming like this, AFAIK Windows is (or at least has been at some point) POSIX compliant.

A standard install of Visual Studio does not make the POSIX header files we need available as part of its include path. Without these the build environment is does not have the POSIX compliance level we need. The windows API calls for threading are available through separate header and will have different naming conventions entirely. If a Windows based build environment were to be setup with the appropriate POSIX header files made available, then it should be possible to make these tests work on Windows.

Technically I believe these these would need a minimum of POSIX.1b for semaphores and POSIX.1c for thread creation and joining. The original POSIX.1 version would not be sufficient. But version POSIX.1-2001 onward would have everything we need.

hannes-steffenhagen-diffblue

Thanks for indulging my nitpicks here

This directory of regression tests is for examples which we intend to use for testing the future work on the analysis of concurrent programs based on a sequentialization approach. Tests which require POSIX specific headers will be disabled for the moment because these are not natively available on Windows. A windows POSIX compatability layer library could potentially be used to enable them to be run on Windows. However the work to do so has not been done.

So that each example can be read separately it its own right.

thomasspriggs force-pushed the tas/pthread_examples branch from 0314878 to d12d57a Compare October 9, 2020 11:21

thomasspriggs requested review from hannes-steffenhagen-diffblue, NlightNFotis and piotr-grabalski October 13, 2020 12:12

piotr-grabalski approved these changes Oct 13, 2020

View reviewed changes

hannes-steffenhagen-diffblue reviewed Oct 14, 2020

View reviewed changes

NlightNFotis suggested changes Oct 14, 2020

View reviewed changes

regression/cbmc-sequentialization/CMakeLists.txt Outdated Show resolved Hide resolved

regression/cbmc-sequentialization/CMakeLists.txt Outdated Show resolved Hide resolved

regression/cbmc-sequentialization/CMakeLists.txt Outdated Show resolved Hide resolved

martin-cs approved these changes Oct 14, 2020

View reviewed changes

thomasspriggs force-pushed the tas/pthread_examples branch from a73d7d7 to 8c8ad9b Compare October 15, 2020 14:07

NlightNFotis approved these changes Oct 15, 2020

View reviewed changes

thomasspriggs force-pushed the tas/pthread_examples branch from c81c4bd to ff6080c Compare October 15, 2020 17:30

hannes-steffenhagen-diffblue reviewed Oct 19, 2020

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Oct 19, 2020

View reviewed changes

thomasspriggs force-pushed the tas/pthread_examples branch from 5275a64 to ddc71fe Compare October 19, 2020 18:45

hannes-steffenhagen-diffblue approved these changes Oct 20, 2020

View reviewed changes

thomasspriggs added 5 commits October 20, 2020 10:49

Add pthreads examples

774c432

Add test using pthread_rwlock

e8ef19a

Duplicate rw_lock code

1a66b57

So that each example can be read separately it its own right.

Add posix semaphore examples

52c0a80

thomasspriggs force-pushed the tas/pthread_examples branch from 79f051d to 52c0a80 Compare October 20, 2020 09:49

thomasspriggs merged commit 9ac232b into diffblue:develop Oct 20, 2020

thomasspriggs deleted the tas/pthread_examples branch October 20, 2020 11:44

		@@ -0,0 +1,29 @@
		if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
		set(gcc_only "-X gcc-only")

Add concurrency examples to regression tests #5521

Add concurrency examples to regression tests #5521

Uh oh!

Conversation

thomasspriggs commented Oct 9, 2020

Uh oh!

codecov bot commented Oct 9, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

piotr-grabalski left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Oct 14, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Oct 14, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Oct 14, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

thomasspriggs commented Oct 15, 2020

Uh oh!

martin-cs commented Oct 15, 2020

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Oct 9, 2020 •

edited

Loading

piotr-grabalski left a comment •

edited

Loading

hannes-steffenhagen-diffblue Oct 14, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Oct 14, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Oct 14, 2020 •

edited

Loading