diff options
Diffstat (limited to 'src/third_party/wiredtiger/tools/litmus_tests')
5 files changed, 0 insertions, 68 deletions
diff --git a/src/third_party/wiredtiger/tools/litmus_tests/README.md b/src/third_party/wiredtiger/tools/litmus_tests/README.md deleted file mode 100644 index 397176de0f8..00000000000 --- a/src/third_party/wiredtiger/tools/litmus_tests/README.md +++ /dev/null @@ -1,15 +0,0 @@ -# WiredTiger litmus tests -In order to support lock free algorithms in the WiredTiger codebase, we define a number of litmus test. These test are intended to be run by the herd7 simulator. - -For any algorithm which has defined litmus tests they can be found under that algorithm's subdirectory. - -To run the litmus tests either install and run herd7, instructions [here](https://github.com/herd/herdtools7/blob/master/INSTALL.md). Or run them from the web interface found [here](http://diy.inria.fr/www/#). - -If a litmus test is required for X86 there should be one defined for ARM64 as well. The reverse is not neccesarily true as X86 has a stronger memory model than ARM. - -### Litmus test style in WiredTiger -WiredTiger litmus tests must use spaces and not have any tabs in the file. There needs to be a single whitespace between the intial state definition block {}, and the process definition block. There must also be an additional whitespace line before the exists clause. - -Test names should be separated with underscores, e.g. wt_gen_drain. - -Additionally per WiredTiger's usual style there should be a newline at the end of the file. diff --git a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_drain_arm64.litmus b/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_drain_arm64.litmus deleted file mode 100644 index bfa2994919f..00000000000 --- a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_drain_arm64.litmus +++ /dev/null @@ -1,14 +0,0 @@ -AArch64 wt_gen_drain -{ -conn_gen=5; -0:X0=conn_gen; 0:X1=sess_gen; -1:X0=conn_gen; 1:X1=sess_gen; -} - - P0 | P1 ; - MOV X9, #1 | LDR X2, [X0] ; - ldaddal X9, X2, [X0] | STR X2, [X1] ; - LDR X2, [X1] | dmb ish ; - | LDR X3, [X0] ; - -exists (0:X2=0 /\ 1:X2=5 /\ 1:X3=5) diff --git a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_drain_x86.litmus b/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_drain_x86.litmus deleted file mode 100644 index 9a8251847e7..00000000000 --- a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_drain_x86.litmus +++ /dev/null @@ -1,12 +0,0 @@ -X86 wt_gen_drain -{ -conn_gen=5; -} - - P0 | P1 ; - LOCK; ADD [conn_gen], $1 | MOV EAX,[conn_gen] ; - MOV EAX, [sess_gen] | MOV [sess_gen], EAX ; - | MFENCE ; - | MOV EBX,[conn_gen] ; - -exists (0:EAX=0 /\ 1:EAX=5 /\ 1:EBX=5) diff --git a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_oldest_arm64.litmus b/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_oldest_arm64.litmus deleted file mode 100644 index 2f8e1a2da6c..00000000000 --- a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_oldest_arm64.litmus +++ /dev/null @@ -1,15 +0,0 @@ -AArch64 wt_gen_oldest -{ -conn_gen=5;sess_gen=0; -0:X0=conn_gen; 0:X1=sess_gen; -1:X0=conn_gen; 1:X1=sess_gen; -2:X0=conn_gen; 2:X1=sess_gen; -} - - P0 | P1 | P2 ; - LDR X2, [X0] | LDR X2, [X0] | MOV W9, #1 ; - dmb ishld | STR X2, [X1] | ldaddal W9, W1, [X0] ; - LDR X3, [X1] | dmb ish | ; - | LDR X4, [X0] | ; - -exists (0:X2=6 /\ 0:X3=0 /\ 1:X2=5 /\ 1:X4=5) diff --git a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_oldest_x86.litmus b/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_oldest_x86.litmus deleted file mode 100644 index 3dc6e8fbde7..00000000000 --- a/src/third_party/wiredtiger/tools/litmus_tests/generations/gen_oldest_x86.litmus +++ /dev/null @@ -1,12 +0,0 @@ -X86 wt_gen_oldest -{ -conn_gen=5; -} - -P0 | P1 | P2 ; -MOV EAX, [conn_gen] | MOV EAX,[conn_gen] | LOCK; ADD [conn_gen], $1 ; -MOV EBX, [sess_gen] | MOV [sess_gen], EAX | ; - | MFENCE | ; - | MOV EBX,[conn_gen] | ; - -exists (0:EAX=6 /\ 0:EBX=0 /\ 1:EAX=5 /\ 1:EBX=5) |