Reintroduced examples

_OCamlProject

@@ -64,23 +64,25 @@ ML_SOURCES:
 	examples/transactional_consistency/snapshot_isolation/snapshot_isolation_code.ml
   examples/transactional_consistency/snapshot_isolation/util/util_code.ml
   examples/transactional_consistency/snapshot_isolation/examples/deprecated/anomalie/anomalie_code.ml
-	examples/transactional_consistency/snapshot_isolation/examples/deprecated/classical_example/classical_example_code.ml
+	examples/transactional_consistency/snapshot_isolation/examples/classical_example/classical_example_code.ml
 	examples/transactional_consistency/snapshot_isolation/examples/deprecated/classical_example_run/classical_example_run_code.ml
-	examples/transactional_consistency/snapshot_isolation/examples/deprecated/function_call/function_call_code.ml
+	examples/transactional_consistency/snapshot_isolation/examples/function_call/function_call_code.ml
 	examples/transactional_consistency/snapshot_isolation/examples/causality_example/causality_example_code.ml
-	examples/transactional_consistency/snapshot_isolation/examples/deprecated/only_reads/only_reads_code.ml
-	examples/transactional_consistency/snapshot_isolation/examples/deprecated/disjoint_writes/disjoint_writes_code.ml
+	examples/transactional_consistency/snapshot_isolation/examples/only_reads/only_reads_code.ml
+	examples/transactional_consistency/snapshot_isolation/examples/disjoint_writes/disjoint_writes_code.ml
   examples/transactional_consistency/snapshot_isolation/examples/sequential_writes/sequential_writes_code.ml
 	examples/transactional_consistency/snapshot_isolation/examples/read_skew/read_skew_code.ml
   examples/transactional_consistency/snapshot_isolation/examples/write_skew/write_skew_code.ml
 	examples/transactional_consistency/snapshot_isolation/examples/bank_transfer/bank_transfer_code.ml
   examples/transactional_consistency/snapshot_isolation/examples/non_repeatable_read/non_repeatable_read_code.ml
-  examples/transactional_consistency/snapshot_isolation/examples/deprecated/no_serializability/no_serializability_code.ml
+  examples/transactional_consistency/snapshot_isolation/examples/no_serializability/no_serializability_code.ml
 	examples/transactional_consistency/snapshot_isolation/examples/deprecated/disjoint_reads/disjoint_reads_code.ml
 	examples/transactional_consistency/snapshot_isolation/examples/deprecated/read_your_writes/read_your_writes_code.ml
 	examples/transactional_consistency/read_committed/examples/dirty_read/dirty_read_code.ml
 	examples/transactional_consistency/read_committed/examples/commit_order/commit_order_code.ml
 	examples/transactional_consistency/read_uncommitted/examples/read_uncommitted_data/read_uncommitted_data_code.ml
+	examples/transactional_consistency/read_uncommitted/examples/read_own_data/read_own_data_code.ml
+
 
 ML_DEPENDENCIES:
 

aneris/examples/transactional_consistency/read_uncommitted/examples/read_own_data/read_own_data_code.v

@@ -0,0 +1,32 @@
+(* This file is automatically generated from the OCaml source file
+<repository_root>/ml_sources/examples/transactional_consistency/read_uncommitted/examples/read_own_data/read_own_data_code.ml *)
+
+From aneris.aneris_lang Require Import ast.
+From aneris.aneris_lang.lib.serialization Require Import serialization_code.
+From aneris.examples.transactional_consistency.snapshot_isolation Require Import snapshot_isolation_code.
+From aneris.examples.transactional_consistency.snapshot_isolation.util Require Import util_code.
+
+Definition transaction1 : val :=
+  λ: "cst", start "cst";;
+             write "cst" #"x" #1;;
+             commitU "cst".
+
+Definition transaction2 : val :=
+  λ: "cst",
+  start "cst";;
+  write "cst" #"x" #2;;
+  let: "vx" := read "cst" #"x" in
+  assert: ("vx" = (SOME #2));;
+  commitU "cst".
+
+Definition transaction1_client : val :=
+  λ: "caddr" "kvs_addr",
+  let: "cst" := init_client_proxy int_serializer "caddr" "kvs_addr" in
+  transaction1 "cst".
+
+Definition transaction2_client : val :=
+  λ: "caddr" "kvs_addr",
+  let: "cst" := init_client_proxy int_serializer "caddr" "kvs_addr" in
+  transaction2 "cst".
+
+Definition server : val := λ: "srv", init_server int_serializer "srv".