Open tobias-schuele opened 7 years ago
Comments from JIRA:
The source code of the test is in the branch embb530_linearizability_tester. I also added a project on Jenkins which will be run nightly. For the moment, the test only checks stacks and queues.
Can the file lt.cpp be split so that the EMBB specific parts are separated from the checker?
Actually only very few lines of lt.cc are strictly related to EMBB. However, a meaningful splitting can perhaps be done. I will try to do it.
I remembered that I did not apply the checker to the single producer single consumer queue. I had to modify the already existing test for queues because it assumed multiple producers multiple consumers. Anyway, the changes are on the branch embb530_linearizability_tester and the test now run on Jenkins. See https://github.com/siemens/embb/commit/8760a84791fb6dbd9e72c1328229c54004ddf8ad and https://github.com/siemens/embb/commit/66fabda7245d6d77720c1bfe0ec5a962ee19bc81
Currently, the linearizability checker from https://github.com/ahorn/linearizability-checker is run on branch embb530_linearizability_tester.