Skip to content

Draft: New subcategory: Termination concurrent

Frank Schüssele requested to merge ultimate-pa/sv-benchmarks:termination-concurrent into main

I want to introduce a new subcategory for the termination of concurrent programs. Therefore I tried to label the existing programs of ConcurrencySafety-Main.set with a termination property. Since we recently got support for the termination of concurrent programs in ULTIMATE, I used the ULTIMATE result as the verdict (some simpler programs were labeled manually). You can find the results here (Note: All benchmarks in this run are labeled with true, therefore the incorrect false results just mean that the program is not terminating).

  • I excluded some folders from ConcurrencySafety-Main.set, namely those where every program does not contain for or while or where ULTIMATE does not provide any result at all. I created a new set-file Termination-Concurrent.set for those categories.
  • Previously exactly one concurrent benchmark was labeled with a termination property (pthread-atomic/gcd-2.yml) and was in the set-file Termination-Other.set. This property was incorrect, so I fixed it and the corresponding folder from the set-file (since it is now contained in Termination-Concurrent.set).
  • Some of the labeled benchmarks do not contain any loops, so I am unsure, if we should keep or remove those.
  • Some of the benchmarks might not be ideal for termination (they were made for safety of course), but we might add some more interesting benchmarks afterwards. This MR should just be starting point for this new subcategory.

Additionally I added some manual verdicts where ULTIMATE failed to provide a result. Here are some small explanations on these commits:

  • e3de70a2: ULTIMATE proved the same benchmarks with less threads (airline-5.yml and floating_read-5.yml) to be terminating.
  • 9fbb38ad: As the name suggests: These benchmarks contain no while-loops, only for-loops. This was found using some syntactic search.
  • 0a6300a0 and 2df658e3: These benchmarks have the pattern while (i<n) { s; i++; }, where s does not modify the variable i, nor does any other thread.
  • 49a6030a:
    • test-hard1.wvr.yml: We were able to prove termination for a simplified version of the program.
    • parallel-misc-5.wvr.yml: This program does not terminate, since it does not reach its (almost "unguarded") error location
  • 8ebfdfc6: All those benchmarks have the same pattern and we have proven a simplified version of those programs to be non-terminating. This is the case, if one of the xi has the value 2^31 at some point due to the overflow.
  • e6fd2d4e: We were able to prove non-termination for a simplified version of the program.
  • e59d5c46: We were able to prove (non-)termination for simplified versions of those programs.
Edited by Frank Schüssele

Merge request reports