История изменений

без формального доказательства это болтовня

Ты когда-нибудь пробовал формально доказать хоть три строчки lock-free кода с доступом к двум ячейкам? У меня где-то валялось формальное доказательство корректности алгоритма lock-free очереди на десяток строк кода — что-то вроде двух страниц текста доказательства. Выделение-высвобождение памяти, естественно, осталось за кадром в виде безупречно работающего черного ящика.

Это сложная задача даже для нескольких строчек, а у меня RW-блокировка занимает примерно 600-700 строк! Формальное доказательство этого кода влезет в томик на один-два килограмма.

без формального доказательства это болтовня

Ты когда-нибудь пробовал формально доказать хоть три строчки lock-free кода с доступом к двум ячейкам? У меня где-то валялось формальное доказательство корректности алгоритма lock-free очереди на десяток строк кода — что-то вроде двух страниц текста доказательства. Это сложная задача даже для нескольких строчек, а у меня RW-блокировка занимает примерно 600-700 строк! Формальное доказательство этого кода влезет в томик на один-два килограмма.

без формального доказательства это болтовня

Ты когда-нибудь пробовал формально доказать хоть три строчки lock-free кода с доступом к нескольким ячейкам? У меня где-то валялось формальное доказательство корректности алгоритма lock-free очереди на десяток строк кода — что-то вроде двух страниц текста доказательства. Это сложная задача даже для нескольких строчек, а у меня RW-блокировка занимает примерно 600-700 строк! Формальное доказательство этого кода влезет в томик на один-два килограмма.