- 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.
Follow us!
В лучших традициях джаваскрипт фреймворков...
do/call и стрелочка это эмуляция императивщины?
А исполняться это будет через выгрузку в их верифицированный конпелятор си?
Как в реальной жизни эти свойства доказываются? Твоя прога строит граф всех состояний системы? Бд это же асинхронная и недетерминированная система?
Да. Все model-checker'ы так и работают. Но в моём случае состояние системы представлено не конкретно (как в "TLA+", "Promela", "Spin" и "Concuerror", например), а параметрически, в виде системы уравнений. Так веселее. Потом из доказательства про этот граф можно сделать тройку Хоара, а их уже можно как угодно кобенировать.
> Бд это же асинхронная и недетерминированная система?
Именно. Она использует сеть, которая пакеты теряет и т.д. Поэтому результат I/O действия определяется как множество возможных исходов. Опять-таки символьно.
Переменные в ней это что?
Множество решений системы - множество состояний? Это сколько уравнений в системе получается?
Состояния частей системы. Если у тебя в стейте есть переменная, то состояние этой переменной. Если есть сеть, то список in-flight пакетов, и т.д.
> Множество решений системы - множество состояний?
Да.
> Это сколько уравнений в системе получается?
Экспоненциально много, иначе никак ^___~ Сейчас пилю оптимизацию про сокращение этого добра примерно на порядок, через знание о том, какие операции коммутируют.
В оптимизированной там формально верифицированный адок.
у тебя есть какая-то модель из состояний и ограничений которая описывает систему, ты из нее строишь систему уравнений, решаешь и получаешь множество вершин графа. А откуда у тебя берется множество ребер?
Из кода выше. "TE" (Trace Event) это и есть ребро графа. "list TE" — список сисколлов процесса (как если к нему strace'ом подрубиться). Он получается раскукоживанием кода из OP-поста. (На самом деле это и не код вовсе, а структура данных хитрая, которая кодирует все возможные поведения процесса).
Ты запускаешь бд, у тебя появляется высер из логов, ты его перемешиваешь и что-то доказываешь?
Лоол. У них то питух то куритса.