gо
Нельзя доказать отсутствие race conditions
Size: a a a
2021 May 31
gо
Это логическая ошибка
[
Можно доказать присутствие, а отсутствие доказательства принять как доказательство отсутвия!
П
Разве что в однопоточном хеллоуворлде
r
Это про доказательства отсутствия? Или конкретно про race conditions?
gо
Второе
gо
race condition это логическая ошибка
r
Хм. А что это значит?
gо
У тебя нет чёткой формулировки «что такое race condition»
NL
Доказать отсутствие race condition достаточно просто: нужно перечислить условия, при которых race condition гарантированно не случается и доказать соблюдение этих условий.
Непонятно, в чём тут логическая ошибка.
Непонятно, в чём тут логическая ошибка.
NL
Оно и не нужно.
gо
Оно нужно, если ты хочешь хоть что-то доказать
r
А чем eventual thread progress, eventual total progress не подходят? "Progress" нужно будет доопределять для конкретных задач.
gо
Самый простой контраргумент тут «большая часть race conditions происходит в взаимодействии с внешними сервисами, код которых мы проверить не можем»
NL
Не нужно.
Нужно формализовать модель памяти, отношение happens-before или чего-то такого, и сформулировать достаточные условия отсутствия race condition.
Нужно формализовать модель памяти, отношение happens-before или чего-то такого, и сформулировать достаточные условия отсутствия race condition.
gо
Это про data races
gо
Data races избежать можно
gо
Rust это делает, например
gо
Race conditions нет
ΑZ
откуда там возьмутся мллионы человекочасов