more data structures

[cdsspec-compiler.git] / benchmark / read-copy-update / rcu.cc

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
new file mode 100644 (file)
index 0000000..ba8b9bd
--- /dev/null
+++ b/benchmark/read-copy-update/rcu.cc
@@ -0,0 +1,85 @@
+#include <atomic>
+
+using namespace std;
+
+/**
+       This is an example about how to specify the correctness of the
+       read-copy-update synchronization mechanism.
+*/
+
+// Properties to check: 
+
+
+typedef void* (*read_func_ptr_t)(void*);
+
+template <typename Type>
+class rcu {
+       /**
+               @Begin
+               @Global_define:
+                       Type *__cur_data;
+
+                       static bool equals(void *ptr1, void *ptr2) {
+                               // ...
+                               // Return if the two data instances pointed to equals to each
+                               // other
+                       }
+
+               @Happens-before:
+                       Write -> Read
+                       Write -> Write
+               @End
+       */
+private:
+       atomic<Type*> _data;
+       
+       public:
+       /**
+               @Begin
+               @Interface: Read
+               @Commit_point_set: Read_Success_Point
+               @Action:
+                       @Code:
+                       void *_Old_Data = __cur_data;
+               @Post_check:
+                       equals(__RET__, _Old_Data->read())
+               @End
+       */
+       void* read() {
+               void *res = NULL;
+               Type *cur_data_ptr = _data.load(memory_order_acquire);
+               /**
+                       @Begin
+                       @Commit_point_check_define: true
+                       @Label: Read_Success_Point
+                       @End
+               */
+               res = cur_data_ptr->read();
+               return res;
+       }
+
+       /**
+               @Begin
+               @Interface: Write
+               @Commit_point_set: Write_Success_Point
+               @Action:
+                       @Code:
+                       __cur_data = new_data;
+               @End
+       */
+       void write(Type *new_data) {
+               while (true) {
+                       Type *prev = _data.load(memory_order_acquire);
+                       if (_data.compare_exchange_weak(prev, new_data,
+                               memory_order_release, memory_order_release)) {
+                               /**
+                                       @Begin
+                                       @Commit_point_check_define: __ATOMIC_RET__ == true
+                                       @Label: Write_Success_Point
+                                       @End
+                               */
+                               break;
+                       }
+               }
+       }
+};