Change model and make several version of it with different optimizati…

…on and verification possibilities

ydb/library/actors/queues/spin/README.md

@@ -14,7 +14,7 @@ brew install spin gcc
 
 Поиск ошибок в инварианте
 ```
-spin -a queue_slow.pml && gcc -o pan pan.c
+spin -a queue_slow.pml && gcc -O2 -w -o pan pan.c
 ./pan -a -I -m<max search depth> -N <name of invariant>
 ```
 
@@ -32,7 +32,7 @@ ltl no_overflow {
 
 Поиск циклов
 ```
-spin -a queue_slow.pml -DWITH_BLOCKING && gcc -o pan pan.c -DNP
+spin -a queue_slow.pml -DWITH_BLOCKING && gcc -O2 -w -o pan pan.c -DNP
 ./pan -l -I -m<max search depth>
 ```
 

ydb/library/actors/queues/spin/atomics.pml

@@ -0,0 +1,52 @@
+#ifndef BASE_PML
+#define BASE_PML
+
+inline atomic_compare_exchange(location, expected, desired, success) {
+    atomic {
+        if
+        :: location == expected ->
+            location = desired
+            success = true
+        :: else ->
+            success = false
+            expected = location
+        fi
+    }
+}
+
+inline blind_atomic_compare_exchange(location, expected, desired) {
+    atomic {
+        if
+        :: location == expected ->
+            location = desired
+        :: else ->
+            expected = location
+        fi
+    }
+}
+
+inline atomic_load(location, value) {
+    atomic {
+        value = location
+    }
+}
+
+inline atomic_store(location, value) {
+    atomic {
+        location = value
+    }
+}
+
+inline atomic_increment(location) {
+    atomic {
+        location = location + 1
+    }
+}
+
+inline atomic_decrement(location) {
+    atomic {
+        location = location - 1
+    }
+}
+
+#endif // BASE_PML

ydb/library/actors/queues/spin/context_switch.pml

@@ -0,0 +1,21 @@
+
+
+
+#define JUMP_POINT(name) \
+jump_point_ ## name: \
+    goto switching_gate_ ## name; \
+// end of JUMP_POINT
+
+#define RETURN_TO_GATE(name) \
+    goto switching_gate_ ## name; \
+// end of RETURN_TO_GATE
+
+
+#define SWITH_CONTEXT(name) \
+    goto jump_point_ ## name \
+// end of SWITH_CONTEXT
+
+#define SWITHING_GATE(name) \
+switching_gate_ ## name: \
+    skip; \
+// end of SWITHING_GATE

ydb/library/actors/queues/spin/macros.pml

@@ -0,0 +1,35 @@
+#define APPLY_FOR_RANGE_FROM_0_TO_1(MACRO, SEPARATOR) \
+    MACRO(0) \
+// end of APPLY_FOR_RANGE_FROM_0_TO_1
+
+#define APPLY_FOR_RANGE_FROM_0_TO_2(MACRO, SEPARATOR) \
+    APPLY_FOR_RANGE_FROM_0_TO_1(MACRO, SEPARATOR) \
+    SEPARATOR \
+    MACRO(1) \
+// end of APPLY_FOR_RANGE_FROM_0_TO_2
+
+#define APPLY_FOR_RANGE_FROM_0_TO_3(MACRO, SEPARATOR) \
+    APPLY_FOR_RANGE_FROM_0_TO_2(MACRO, SEPARATOR) \
+    SEPARATOR \
+    MACRO(2) \
+// end of APPLY_FOR_RANGE_FROM_0_TO_3
+
+#define APPLY_FOR_RANGE_FROM_0_TO_4(MACRO, SEPARATOR) \
+    APPLY_FOR_RANGE_FROM_0_TO_3(MACRO, SEPARATOR) \
+    SEPARATOR \
+    MACRO(3) \
+// end of APPLY_FOR_RANGE_FROM_0_TO_4
+
+#define APPLY_FOR_RANGE_FROM_0_TO_5(MACRO, SEPARATOR) \
+    APPLY_FOR_RANGE_FROM_0_TO_4(MACRO, SEPARATOR) \
+    SEPARATOR \
+    MACRO(4) \
+// end of APPLY_FOR_RANGE_FROM_0_TO_5
+
+#define APPLY_FOR_RANGE_FROM_0_TO(N, MACRO, SEPARATOR) \
+    APPLY_FOR_RANGE_FROM_0_TO_##N(MACRO, SEPARATOR) \
+// end of APPLY_FOR_RANGE_FROM_0_TO
+
+#define FOR_ALL(N, MACRO) \
+    APPLY_FOR_RANGE_FROM_0_TO(N, MACRO, && ) \
+// end of FOR_ALL

ydb/library/actors/queues/spin/queue_base.pml

@@ -0,0 +1,104 @@
+#ifndef QUEUE_BASE_PML
+#define QUEUE_BASE_PML
+
+#ifndef QUEUE_SIZE
+#define QUEUE_SIZE 4
+#endif
+
+#include "atomics.pml"
+
+typedef Slot {
+    unsigned generation:3;
+    bool isEmpty;
+}
+
+#define EQ_SLOT(slot1, slot2) ((slot1.generation == slot2.generation) && (slot1.isEmpty == slot2.isEmpty))
+
+typedef Queue {
+    unsigned tail:4;
+    unsigned head:4;
+    Slot buffer[QUEUE_SIZE];
+}
+
+#define QUEUE_SLOT(counter) queue.buffer[(counter) % QUEUE_SIZE]
+
+
+inline increment_queue_head(currentHead) {
+    blind_atomic_compare_exchange(queue.head, currentHead, currentHead + 1)
+}
+
+inline increment_queue_tail(currentTail) {
+    blind_atomic_compare_exchange(queue.tail, currentTail, currentTail + 1)
+}
+
+inline invalidate_slot(counter, current_generation) {
+    atomic {
+        QUEUE_SLOT(counter).generation = current_generation + 1;
+        QUEUE_SLOT(counter).isEmpty = true;
+    }
+}
+
+inline save_slot_value(counter, saved_generation) {
+    atomic {
+        QUEUE_SLOT(counter).isEmpty = false;
+        QUEUE_SLOT(counter).generation = saved_generation;
+    }
+}
+
+inline store_slot(counter, new_generation, new_is_empty) {
+    atomic {
+        QUEUE_SLOT(counter).generation = new_generation;
+        QUEUE_SLOT(counter).isEmpty = new_is_empty;
+    }
+}
+
+inline copy_slot(source, destination) {
+    atomic {
+        destination.generation = source.generation;
+        destination.isEmpty = source.isEmpty;
+    }
+}
+
+inline read_slot(counter, destination) {
+    atomic {
+        copy_slot(QUEUE_SLOT(counter), destination);
+    }
+}
+
+inline compare_exchange_slot(counter, expectedSlot, new_generation, new_is_empty, success) {
+    atomic {
+        if
+        :: !EQ_SLOT(expectedSlot, QUEUE_SLOT(counter)) ->
+            read_slot(counter, expectedSlot);
+            success = false;
+        :: else ->
+            success = true;
+            store_slot(counter, new_generation, new_is_empty);
+        fi
+    }
+}
+
+inline JUMP_SLOT_CHANGED(head, slot, label) {
+    if
+    :: !EQ_SLOT(slot, QUEUE_SLOT(head)) ->
+        read_slot(head, slot);
+        goto label
+    :: else -> skip
+    fi
+}
+
+inline init_queue() {
+    atomic {
+        queue.tail = 0;
+        queue.head = 0;
+        int i = 0;
+        do
+        :: i < QUEUE_SIZE -> 
+            invalidate_slot(i, -1);
+            i++
+        :: i >= QUEUE_SIZE -> break
+        od
+    }
+}
+
+#endif // QUEUE_BASE_PML