/извините за продолжение оффтопика/, но мы вывели империческое правило, что если у вас concurrent алгоритм в котором нетривиальное число CAS-ов и у вас нет механически проверенного доказательства его корректности, то вряд ли он корректен. У нас тут ребята делали новый быстрый алгоритм семафора (а это уж намного более простая штука чем deqeue). Несколько экспертов думало и изучало алгоритм, тестов написано вагон. Начали док-во на Coq прикручивать, так сразу нашли несколько багов.

У Tsigas-Sundell тоже «доказательство» есть. Но оно не помогает.

Мне кажется все это должно рашаться на уровне железа. Собственно для этого давно придумали спекулятивные техники вроде Speculative Lock Elision и Transactional Lock Removal (TLR)

Там даже с CAS есть проблемка с ABA. Обычно решается через тегирование

/извините за продолжение оффтопика/, но мы вывели империческое правило, что если у вас concurrent алгоритм в котором нетривиальное число CAS-ов и у вас нет механически проверенного доказательства его корректности, то вряд ли он корректен. У нас тут ребята делали новый быстрый алгоритм семафора (а это уж намного более простая штука чем deqeue). Несколько экспертов думало и изучало алгоритм, тестов написано вагон. Начали док-во на Coq прикручивать, так сразу нашли несколько багов.

(Или там SRW locks) если нужно с нераздельными ресурсами работать то доктор прописал использовать нормальные примитивы синхронизации а не самописные

Всем привет. Кто-то пилил свой фронт-енд для Cranelift? Не пойму как собрать готовый бинарь под хостовый таргет

Или что-то типа lock-free списка реализовать, тогда как мне кажется, если какие-то изменения еще не отразились, то это не должно приводить к ошибкам в работе с очередью.

Обычный спинлок на CAS будет корректен без барьеров на x86 (но нужно использовать CAS, а вы вроде не хотите это делать).
Из экзотики, есть вот такой алгоритм https://en.m.wikipedia.org/wiki/Szyma%C5%84ski%27s_algorithm. Он вроде тоже не требует барьеров, но тут я не до конца уверен :)

но тут еще вопрос что считать C11, там же не одна модель

В с11 вроде стандартизовали модель памяти же?

/извините за продолжение оффтопика/, но мы вывели империческое правило, что если у вас concurrent алгоритм в котором нетривиальное число CAS-ов и у вас нет механически проверенного доказательства его корректности, то вряд ли он корректен. У нас тут ребята делали новый быстрый алгоритм семафора (а это уж намного более простая штука чем deqeue). Несколько экспертов думало и изучало алгоритм, тестов написано вагон. Начали док-во на Coq прикручивать, так сразу нашли несколько багов.

/извините за продолжение оффтопика/, но мы вывели империческое правило, что если у вас concurrent алгоритм в котором нетривиальное число CAS-ов и у вас нет механически проверенного доказательства его корректности, то вряд ли он корректен. У нас тут ребята делали новый быстрый алгоритм семафора (а это уж намного более простая штука чем deqeue). Несколько экспертов думало и изучало алгоритм, тестов написано вагон. Начали док-во на Coq прикручивать, так сразу нашли несколько багов.

В общем, попробовал заменить самописный Деккер на критические секции из Windows и проблема ушла. Спасибо за совет. Еще, кстати, проблема пропадала, если внутри самописной критической секции делать вывод в консоль. А вывод в консоль он тоже сделан через вызов WinApi функций и видимо это тоже как-то связано. Но критические секции в любом случае надежнее, чем консоль.