diff --git a/linearizability_tester/README.txt b/linearizability_tester/README.txt index 8bed8fc..f5dc9ca 100755 --- a/linearizability_tester/README.txt +++ b/linearizability_tester/README.txt @@ -17,14 +17,14 @@ The src folder contains a large part of the code by Alex Horn. COMPILE INSTRUCTIONS * On Linux system -Suppose that the embb library was build in ../build (relative path to the current +We suppose that the embb library was build in ../build (relative path to the current folder of the linearizability test). From within the linearizability_tester folder, cd (or mkdir->cd) into the build directory, then run "cmake .." and "make". The executable of the test should be placed in the same folder with the name EMBB_linearizability_test. * On Windows system -Suppose that the embb library was build in ../build (relative path to the current +We suppose that the embb library was build in ../build (relative path to the current folder of the linearizability test). NOTE: the embb library should be build in Release mode, i.e. by running the command "cmake --build . --config Release" from inside the correct directory. @@ -34,6 +34,20 @@ be used. The executable of the test should be placed in the folder Release with the name EMBB_linearizability_test.exe. -HOW TO IMPLEMENT TESTS FOR OTHER DATASTRUCTURES - -Data structures that support the following functions: \ No newline at end of file +HOW TO IMPLEMENT TESTS FOR OTHER DATA STRUCTURES + +Data structures that support the following functions: +- check if structure is empty +- check if structure contains a specific element +- insert an element in the structure +- erase an element from the structure +should be easily checkable using the Set specification contained in the +src/sequential_datastructures.h file. +In general, the checker needs a sequential implementation test against the +concurrent one (the EMBB one). The implementation should support efficient equality checks +and efficient memory management. Stick to the implementation of the already integrated +structures (stacks, queues..) for future integration. +After adding the implementation of the datastructure, it is necessary to add a worker and +experiment for the newly created datastructure in main.cc. Stick again to the already +implemented functions (it should be sufficient to change the name of the methods that are called +on the EMBB structure). \ No newline at end of file diff --git a/linearizability_tester/src/sequential_data_structures.h b/linearizability_tester/src/sequential_data_structures.h index 40cc468..49c628a 100755 --- a/linearizability_tester/src/sequential_data_structures.h +++ b/linearizability_tester/src/sequential_data_structures.h @@ -1,9 +1,10 @@ +/** +/* Sequential implementation of the datastractures to test +*/ + #ifndef __SEQUENTIAL_DATASTRUCTURES #define __SEQUENTIAL_DATASTRUCTURES -#include - - namespace lt{ namespace state{ class Set diff --git a/linearizability_tester/src/tests.h b/linearizability_tester/src/tests.h index ac95306..950bfce 100755 --- a/linearizability_tester/src/tests.h +++ b/linearizability_tester/src/tests.h @@ -1,3 +1,7 @@ +/** +/* Internal tests for the linearizability checker +*/ + #include #include