Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
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.
Continuations are like violence, if they don't work then you're not using enough of them.
Как-то так, да. "do ret <- action" это Notation для конструктора типа trace event "процесс с пидом Pid выполнил сисколл action, и ему вернулося ret". Потом trace event'ы от разных процессов перемешиваются, и для каждой кобенации решается система уравнений. Eсли она не совместна, то значит кобенация невозможна (к примеру, два процесса входит в одну критическую секцию), если совместна, то она задаёт область пространства состояний системы, про которую можно что-то доказать.
Выгружать во что-то функциональное придётся, ибо этот метод про I/O, а не про memory safety. (В теории и кучу, конечно, можно имитировать через I/O, но зачем)
>safety, а не liveness
Как в реальной жизни эти свойства доказываются? Твоя прога строит граф всех состояний системы? Бд это же асинхронная и недетерминированная система?
Да. Все model-checker'ы так и работают. Но в моём случае состояние системы представлено не конкретно (как в "TLA+", "Promela", "Spin" и "Concuerror", например), а параметрически, в виде системы уравнений. Так веселее. Потом из доказательства про этот граф можно сделать тройку Хоара, а их уже можно как угодно кобенировать.
> Бд это же асинхронная и недетерминированная система?
Именно. Она использует сеть, которая пакеты теряет и т.д. Поэтому результат I/O действия определяется как множество возможных исходов. Опять-таки символьно.
Состояния частей системы. Если у тебя в стейте есть переменная, то состояние этой переменной. Если есть сеть, то список in-flight пакетов, и т.д.
> Множество решений системы - множество состояний?
Да.
> Это сколько уравнений в системе получается?
Экспоненциально много, иначе никак ^___~ Сейчас пилю оптимизацию про сокращение этого добра примерно на порядок, через знание о том, какие операции коммутируют.
я тут пытаюсь себе представить что ты делаешь
у тебя есть какая-то модель из состояний и ограничений которая описывает систему, ты из нее строишь систему уравнений, решаешь и получаешь множество вершин графа. А откуда у тебя берется множество ребер?
Из кода выше. "TE" (Trace Event) это и есть ребро графа. "list TE" — список сисколлов процесса (как если к нему strace'ом подрубиться). Он получается раскукоживанием кода из OP-поста. (На самом деле это и не код вовсе, а структура данных хитрая, которая кодирует все возможные поведения процесса).
Я ничего не запускаю, а создаю структуру данных, описывающаю все возможные последовательности сисколлов (трейс), которые бд (вернее какая-то её подпрограмма) может вызвать. (См. OP-пост, это она). Затем кобенирую её с другими подпрограммами, с которыми она может устраивать гонки данных, и получаю экспоненциально большой набор трейсов уже от двух параллельных потоков. Затем я проверяю, возможен ли физически каждый трейс, если он возможен — что-то про него доказываю.
CHayT # 0
Cnapmak # 0 ⇈
Desktop # 0 ⇈
Pig # 0
bormand # 0
В лучших традициях джаваскрипт фреймворков...
do/call и стрелочка это эмуляция императивщины?
CHayT # 0 ⇈
bormand # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
А исполняться это будет через выгрузку в их верифицированный конпелятор си?
CHayT # 0 ⇈
bootcamp_dropout # 0 ⇈
Как в реальной жизни эти свойства доказываются? Твоя прога строит граф всех состояний системы? Бд это же асинхронная и недетерминированная система?
CHayT # 0 ⇈
Да. Все model-checker'ы так и работают. Но в моём случае состояние системы представлено не конкретно (как в "TLA+", "Promela", "Spin" и "Concuerror", например), а параметрически, в виде системы уравнений. Так веселее. Потом из доказательства про этот граф можно сделать тройку Хоара, а их уже можно как угодно кобенировать.
> Бд это же асинхронная и недетерминированная система?
Именно. Она использует сеть, которая пакеты теряет и т.д. Поэтому результат I/O действия определяется как множество возможных исходов. Опять-таки символьно.
bootcamp_dropout # 0 ⇈
Переменные в ней это что?
Множество решений системы - множество состояний? Это сколько уравнений в системе получается?
CHayT # 0 ⇈
Состояния частей системы. Если у тебя в стейте есть переменная, то состояние этой переменной. Если есть сеть, то список in-flight пакетов, и т.д.
> Множество решений системы - множество состояний?
Да.
> Это сколько уравнений в системе получается?
Экспоненциально много, иначе никак ^___~ Сейчас пилю оптимизацию про сокращение этого добра примерно на порядок, через знание о том, какие операции коммутируют.
bootcamp_dropout # 0 ⇈
CHayT # 0 ⇈
В оптимизированной там формально верифицированный адок.
bootcamp_dropout # 0 ⇈
у тебя есть какая-то модель из состояний и ограничений которая описывает систему, ты из нее строишь систему уравнений, решаешь и получаешь множество вершин графа. А откуда у тебя берется множество ребер?
bormand # 0 ⇈
CHayT # 0 ⇈
Из кода выше. "TE" (Trace Event) это и есть ребро графа. "list TE" — список сисколлов процесса (как если к нему strace'ом подрубиться). Он получается раскукоживанием кода из OP-поста. (На самом деле это и не код вовсе, а структура данных хитрая, которая кодирует все возможные поведения процесса).
bootcamp_dropout # 0 ⇈
Ты запускаешь бд, у тебя появляется высер из логов, ты его перемешиваешь и что-то доказываешь?
CHayT # 0 ⇈
bootcamp_dropout # 0 ⇈
bormand # 0 ⇈
CHayT # 0 ⇈
bootcamp_dropout # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
Лоол. У них то питух то куритса.
bootcamp_dropout # 0 ⇈
CHayT # 0 ⇈