Scala 2022-07-04 10:11

В том числе. Вот примерный список проблем, которые хочет решить этот jep:
1) не все существующие методы чтения-записи формализованы в jmm
2) текущую jmm не переваривают автоматические верификаторы
3) есть немалая вероятность, что в текущей jmm присутствуют ошибки
4) текущая jmm невероятно сложная

Интересно будет на процесс посмотреть

Чем и как будут формализовать

А то есть только несколько хелловорлд левел формализаций на коке

По-моему даже с использованием чего-то уровня iris я не видел

Прикольно было бы если бы клайрат с наневским взяли бы и как нахоарили в жаву

чот цитата про «невероятно сложная» не оч воодушевляет 🙂

подозреваю что там работы на отдельный грант

глаза боятся, елаборации делают

наверное больше

ну нам бы простое для начала научиться нахоаривать как-то канонично

ну и 100% ломание таких китов сломает весь жава софтвер в мире

а то щас нахоарить интервал-линеаризуемость для java.util.concurrent.Exchanger это работы на полгода-год

а я думал там
> Неет ты не можешь просто найти пруфнуть или опровергнуть JMM
> Хаха, хоар тактика делает qed qed

ну у нас же идея делать все максимально низкоуровнево

типа, руками копать символьные трассы

чтобы наработать таким образом какие-то типо-алгебраические паттерны для 🐎карренси

так что никаких тактик, максимум отрефлексированные солверы на канструктурах

поэтому проект так и называется — Type and Proof Structures for Concurrent Software Verification

Чтобы получить грант, надо больше хорохоариться, мол, сейчас все верифицируем