- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
Definition read_t key cont : Thread :=
call tx_context <- get_tx_context;
call cell <- get_cell key tx_context;
match cell.(cell_write) with
| Some v =>
do _ <- log (read key v);
cont v
| None =>
do v <- read_d key;
let tx_context' := set tx_cells <[key := cell]> tx_context in
do _ <- pd_set tx_context';
do _ <- log (read key v);
cont v
end.