Комментарии 40
А вот Глобуляром овладейте, это гораздо веселее
https://golem.ph.utexas.edu/category/2015/12/globular.html
Я с начала 90-х был увлечён теорией типов. И последнее время ощущение "хватит, так нельзя, это НЕКРАСИВО". С этим бухгалтером мы ещё намучаемся, как сказал Бисмарк, прочитав "Капитал".
Прошу прощения за лёгкий оффтоп.
Где можно найти живую площадку по этому инструменту? А то начал смотреть и у меня возникли вопросы, например, почему на диаграмме cusp 1 (3-клетка между 2-клетками CupBR и CupRB, которые имеют вид B→R и R→B, соответственно, где B и R — выделенные 1-клетки общей 0-клетки) в режиме Project 1 весь фон, в том числе между CupBR и CupRB, закрашен в красный, то есть в R, а не в синий (B), как того ожидал бы я?
И всё это из-за того, что кто-то решил писать приложение на C и атомиках. А ведь можно же было взять Go, использовать более высокороувневые примитивы чем атомики, запускать тесты с go test -race… и скольких проблем бы удалось избежать! :)
Скорее, MC полезен для авторов библиотек - тех самых высокоуровневых примитивов. Угадайте, что внутри реализаций высокоуровневых примитивов? Код на Go, высокоуровневые примитивы, вы думаете? И так turtles all the way down? Я так не думаю.
Ну, вообще-то почти. Внутри примитивов всё ещё код на Go (https://cs.opensource.google/go/go/+/refs/tags/go1.17.3:src/sync/mutex.go;l=72) а под ним буквально 6 строк на ассемблере (https://cs.opensource.google/go/go/+/refs/tags/go1.17.3:src/runtime/internal/atomic/atomic_amd64.s;l=22-36).
Но Вы упустили главное - в конце моего комментария стоял смайлик.
Ну вот, 226 строк низкоуровневого Go плюс внизу 6 строк на ассемблере - проверены вручную или формально, разница существенна. Про смайлик - в очном разговоре иронию легче уловить благодаря интонации и мимике, на письме (особенно в общении с случайным собеседником) - сложнее; да, смайлик я пропустил.
Автору - спасибо, интересно - про GenMC раньше не слышал (последний раз искал по теме - нашлись книги по TLA+ и Alloy, довольно старые системы).
Сколько времени займёт формальная проверка всего этого низкоуровневого кода? И сколько времени будет требоваться на её обновление и перепроверку при каждом изменении (в основном - нетривиальных оптимизациях)?
Мне интересна данная тема, но в практическую применимость этого подхода в реальных проектах я не очень верю, даже если это не средний коммерческий говнокодпроект а вполне себе крутой и вылизанный рантайм языка Go.
Точнее, практическая применимость доступная на сегодняшний день - это как раз вышеупомянутый go test -race. Который работает сам, из коробки, и не требует от разработчиков ни одной лишней строки кода (не считая обычных тестов). Да, его результаты не настолько совершенны, но зато от него уже сегодня есть польза реальным проектам.
Здесь был товарищ, который себе на Coq'е, вроде, вполне себе денежку в Америках зарабатывает:
@0xd34df00d
Я не хотел бы ввязываться в жаркий спор о рантайме Go, с которым я не знаком и не собираюсь знакомиться в ближайшее время. Тем не менее, считаю беседу достаточно содержательной для добавлении ещё одной реплики.
Я бегло просмотрел информацию про "go test -race" - вещь, безусловно, полезная и доступная - однако, насколько я понял, она хороша настолько, насколько хорошо тестовое покрытие. Да, документация с осторожностью рекомендует возможность запускать каких-то случаях (поиск production багов, не пойманных тестами?) и в production - предупреждая, что "The cost of race detection varies by program, but for a typical program, memory usage may increase by 5-10x and execution time by 2-20x."
Насчёт баланса стоимости и эффекта статического анализа: просмотрел довольно объёмную статью про использование MC-анализа для real world проблемы (не вникая в детали - я сам TLA+ не использовал, знаком с этим инструментом вприглядку - но кое-где не очень далеко от моего места работы этот инструмент содержательно использовался). Идёт речь о ловле и исправлении deadlock бага в реализации condition variable в стандартной библиотеке C. Может, вам тоже будет любопытно просмотреть. Стандартная библиотека C - довольно критически важная и стабильная база кода (впрочем, я подозреваю, что корректность реализации mutex.go тоже довольно критически важна, а последнее изменение в mutex.go было внесено 3 года назад). Статья годичной давности: Using TLA+ in the Real World to Understand a Glibc Bug | Probably Dance. Автор, скорее всего, работает в геймдеве, и с проблемой работал не из досужего интереса.
Поправьте меня, если я что-то не так понял, но "применимость в реальном мире" звучит примерно так:
Есть буквально 2-3 экрана кода, где есть сложноуловимый баг, и глазами мы его найти не в состоянии.
Мы тратим дофига времени переводя эти 2-3 экрана кода в запись, которую можно проверить формально…
Профит! Ещё не прошло и месяца, а баг найден.
Если я всё понял правильно, то у меня для Вас плохая новость: обычно есть гораздо более простой способ решения этой проблемы.
Есть две основные причины, по которым баг не получается обнаружить не смотря на все прилагаемые усилия: недостаточная квалификация (из-за которой в голове некорректная картина как всё работает) и неспособность понять весь алгоритм целиком (не влазит в голову). Первая причина лечится обучением (или передачей задачи тому, кто лучше ориентируется в теме). Вторая причина лечится переписыванием алгоритма так, что он стал проще для понимания и поместился в голову. Оба лекарства крайне положительно сказываются и на разработчике и на коде, поэтому я бы не рекомендовал прибегать к формальной верификации кода с целью избежать приёма этих лекарств. :)
А еще есть алгоритмы, которые целиком в голову не помещаются. Или помещаются, но только в очень умные головы, которые уже нашли применение своим головам где-то в других стратосферах.
Нету таких. Любой алгоритм можно и нужно декомпозировать до состояния, пока он не поместится в абсолютно среднюю голову. И пока он не помещается - его рано даже начинать кодить!
Что до очень умных голов, то на этот счёт есть очень хорошее наблюдение (цитируя Кернигана): "Отладка кода вдвое сложнее, чем его написание. Так что если вы пишете код настолько умно, насколько можете, то вы по определению недостаточно сообразительны, чтобы его отлаживать.". Так что нет, очень умная голова - это не решение, это плюс ещё одна проблема. Потому что код-то она напишет, а вот что с этим кодом потом дальше делать…
Что вы, наличие более простого способа решения проблемы - всегда хорошая новость! Жаль, никто не смог в данном случае этого сделать... Так что, увы, хорошей новости не случилось.
В этом случае (deadlock баг в реализации conditional variable в glibc), похоже, простой способ почему-то не сработал. Сложный - сработал. И это не единственный случай, когда для решения реальной проблемы пришлось прибегнуть к сложному способу.
Для меня это (необходимость применения в некоторых сложных случаях сложных способов) - не новость. Для вас - плохая новость?
Сожалею, что оставил реплику со ссылкой на статью по проблеме с glibc - получил порцию нотаций от незнакомого человека, которых почему-то решил снисходительно поучить меня жизни и профессии.
Всего доброго.
Я прошу прощения, если Вы так это восприняли - ни нотаций ни снисхождения я в этот комментарий не вкладывал и не имел в виду ничего подобного.
Я действительно пытаюсь разобраться в пределах применимости описанного в статье подхода. Поэтому я и начал с "поправьте меня, если я что-то не так понял" - это была не фигура речи а просьба. Я не владею данным инструментом и действительно могу чего-то важного не понимать - это вообще-то нормально при настолько поверхностном знакомстве, было бы странно, если бы я, наоборот, сходу в нём разобрался.
Тон того комментария действительно провоцирующий, но цель этого не обидеть Вас, а… спровоцировать доказывать свою точку зрения, показать где я неправ, поделиться Вашим опытом. Не на всех это действует именно так, но тут сложно угадать с первой попытки, в каком тоне с кем надо общаться для максимально продуктивной беседы.
На данный момент мне действительно кажется, что сложные для понимания алгоритмы полезнее декомпозировать и упрощать, а не применять ещё более сложные инструменты для компенсации своей неспособности разобраться. И да, я искренне уверен, что декомпозировать и упростить возможно всегда - это не всегда легко получается, но если принять что это обязательно и пока это не будет проделано код писать нельзя - обычно решение находится. И я очень хочу услышать где я ошибаюсь, какие альтернативные подходы в каких ситуациях работают лучше. Ну или не лучше, а просто хоть как-то работают, в отличие от всех остальных подходов включая вышеупомянутый.
Тем не менее, не смею настаивать на продолжении беседы и ещё раз прошу прощения.
Хорошо, давайте обсудим, и я извиняюсь за эмоциональность. Давайте оставим в стороне кейс с glibc. Я поясню, почему интересуюсь именно TLA+ (по названию инструмента нашёл кейс).
Один повод - тот факт, что высоконагруженная система не всегда даёт лучшие показатели с высокоуровневыми примитивами параллелизма. Приходится использовать lock-free структуры данных (не знаю, как с ними в Go, на C в стандартную библиотеку не входят), и я не уверен, что мне не придётся ловить / отлаживать баг, подобный описанному в том блог посте про glibc. Да, пока обходился без глубокого знакомства с инструментом, но знаю, что он использовался неподалёку - именно из-за сложностей с редко воспроизводящимися, но причиняющими постоянную боль багами с параллелизмом.
Далее, любопытный фрагмент истории инструмента (тут я могу быть не вполне точным, печатаю без проверки каждого фактоида). TLA+ разработал Лесли Лампорт (автор среди прочего LaTeX, но в данной истори более кстати тот факт, что он автор алгоритма distributed consensus под названием Paxos). Ему нужно было средство автоматической верификации алгоритмов такого рода и, скорее всего, ни одно из существующих на тот момент не подходило. Реализовав инструмент, он написал книгу, поясняя, как им пользоваться (также, как до этого написал книгу про LaTeX). Другой автор продолжил (хоть инструмент старый, недавняя книга вышла в 2018-м). Короче, я решил хотя бы шапочно познакомиться с TLA+, буду готов, если прийдётся применять (ну и, интересная тема - в школе и институте приходилось формально корректно доказывать теоремы на зачёт / сдачу экзамена).
Давайте для проверки тезиса, что алгоритм (довольно базовый - что может быть базовей достижения консенсуса в распределнной системе, да?) такого класса не будет воспринят серьёзно без формальной верификации, рассмотрим более недавнюю альтернативу Paxos-у, Raft. Да, быстро нашлась статья по верификации Raft-а - верифицировали с использованием Coq, кстати (как в работе автора статьи, в комментариях к которой мы находимся).
Нужно ли это программистам в повседневной работе? Хорошо, если нет! Но, когда всё-таки "не повезло" и таки-нужно, улучшение инструментов не помешает.
Вспомнился другой случай, более прозаический - баг в стандартном алгоритме сортировки Python, TimSort (используемом также в Java-системах, в стандартных коллекциях). Баг существовал в коде алгоритма (портированного вместе с багом для Java) лет 12-13, прикидочно. Его нашли и исправили только тогда, когда computer scientist-ы (уровня аспирантов, я так понимаю) попробовали верифицировать алгоритм (в рамках более крупного проекта верификации стандартных библиотек Java). На Хабре были заметки про это, вот, например (переводная): https://habr.com/ru/post/251751/. Баг, скорее всего, проявлялся довольно редко. Тем не менее, лучше всё-таки, если он исправлен, и корректность исправленного алгоритма, наконец, доказана? Это подводит к тезису, что доказывать корректность стабильных базовых библиотек (в частности, реализующих высокоуровневые примитивы для многопоточного программирования) - неплохая идея.
Насколько это дорого? Учёные делают это "за кредиты" (статьи), и при этом улучшают инструменты (о чём статья, в комментариях к которой мы находимся). Иногда за инструмент приходится браться программисту (пример - случай с glibc). Дороговизну применения инструмента в конкретном случае следуют делить на массовость применения проверяемого алгоритма с учётом возможной высокой стоимости его отказа. Иногда знаменатель оказывается достаточно большой.
Вот бы Haskell Prelude формально верифицировать на Idris 2, Agda 2.
Мне стало любопытно - первым делом нашлась документация о том, как это делается с Coq:
https://www.cis.upenn.edu/~plclub/blog/2020-10-09-hs-to-coq/
Формальное доказательство алгоритмов вроде Raft и Paxos - это вполне уместное применение, согласен. В основном потому, что алгоритм не меняется с каждым коммитом, и доказать его достаточно один раз. В отличие от конкретной реализации.
Развлечения учёных тоже вполне штатный кейс, там никогда вопрос цены не был определяющим фактором, а шанс на получение практической пользы всегда был довольно непредсказуемым.
А вот для практических задач, включая кейс с glibc - цена явно не выглядит адекватной и подход явно не рекомендован к применению со всеми сложными багами.
Я как-то писал сервис, который тянул миллион одновременных подключений на одном сервере - это было давно, но, если не путаю, то там было достаточно отказаться от совсем уж высокоуровневых примитивов Go (каналов), использовать вместо них обычные мьютексы плюс применить lock striping (названия этой техники я тогда не знал, но идея очевидная и придумалась сама). В целом, по моим наблюдениям, этого подхода хватает с головой для абсолютного большинства задач с высокими нагрузками. Тормоза обычно (по крайней мере, во всех известных мне случаях) вызваны кривым проектированием данных и алгоритмов, а вовсе не тем, что мьютексы не справляются. Я понимаю, что наверняка существует небольшое количество проектов-исключений из вышесказанного, но абсолютное большинство разработчиков с такими никогда не столкнётся.
Иными словами, больше всего пока похоже на то, что знать о возможности что-то формально доказать любопытно, но практическое применение в ежедневной разработке софта для него отсутствует. :(
На данный момент мне действительно кажется, что сложные для понимания алгоритмы полезнее декомпозировать и упрощать, а не применять ещё более сложные инструменты для компенсации своей неспособности разобраться.Это нужно, чтобы не полагаться на добросовесность разработчиков(вдруг кто-то бекдор послал в виде испралвения?), а так же на то, что разработчики не действовали в спешеке, выспались и так далее.
Хорошо. Мы соглашаемся о пользе доказательства правильности каких-то стабильных алгоритмов. Однако, используемые для этого средства приносят пользу и в ежедневной рутине, и я попробую привести простой пример.
Что вы говорите, пишете коллеге, реализовавшем цикл, в котором непонятно, почему произойдёт завершение, и будет ли при завершении гарантирован какой-либо результат?
Используете ли вы в таком случае в диалоге термины вроде "инвариант цикла", "условие завершения"? Не предлагаете ли вы такому коллеге от греха подальше пользоваться более выскоуровневыми конструкциями типа range loop (специально проверил, что в Go есть такой)?
Если да, то - и для вашей практической пользы "учёные развлекались не зря" (какое-то время назад эти понятия не существовали, и какое-то время заняло признание их полезности большинством активных программистов, имеющих дело с циклами).
Однако, у вас где-то проведена черта: до неё учёные развлекались не зря, а после неё - ну вот это уже выпендриваются. И вы считаете, что эта черта должна у всех программистов в голове наличествовать, и проходить достаточно близко к той, которая в голове у вас. Мы зацепились из-за этого, похоже.
Сознаюсь, мой интерес к теме обусловлен тем, что такие темы, как в этой статье, поддерживают мой интерес к профессии в целом. Мотивирую себя чтением интересных мне статей не бросать эту профессию - даже если практического применения в моей сегодняшней работе нет. И, кстати, прогресс наблюдаю - тот же ваш любимый Go с его замечательными высокоуровневыми примитивами не возник бы без предшествующей продуктивной работы учёных и интереса промышленных программистов к их наработкам.
Обратный пример, отрицательный, но он вам должен быть близок. Perl - замечательный язык программирования, с высокоуровневыми конструкциями и компактной записью программ. Практичный (мой любимый пример - в "научной" терминологии ассоциативный массив, словарь или map - честно назван в ядре языка hash, ну чтобы сразу практичному программисту было понятно, что там внутри). У него были замечательные перспективы, активная аудитория практикующих программистов. На нём было легко создавать работающие программы! Более того, этот язык был создан начинающим программистом - и исходя из его практических потребностей (замечу, эта история создания языка программирования отличается от истории создания Go). Когда и что с Perl пошло не так, как вы считаете? Я недавно узнал, язык переименовали... зачем - может быть, чтобы сбросить балласт каких-то отрицательных коннотаций? Но что конкретно?! У вас есть мнение на этот счёт? Мне, честно говоря, Perl не нравился, но я никогда на нём не программировал, так что моё мнение - неквалифицированное. Однако, могу вздохнуть свободно - ныне это название языка могу смело выкидывать из головы (а переименованное даже не трудиться запоминать).
Вы не совсем правильно меня поняли. У меня в голове никакой черты в отношении того, стоит ли учёным "развлекаться" нет, слово "развлекаются" описывает их работу без какой-либо отрицательной коннотации. Зря/не зря просто описывает тот факт, что далеко не всегда результат их работы понятно как использовать на практике, но "зря" никоим образом не подразумевает, что "развлекаться" не стоило.
Просто лично меня интересует не процесс и не все подряд результаты, а только те, которые можно применить на практике. Здесь черта действительно есть, но она не про учёных, а про меня - есть ли для меня польза.
Не совсем понял, зачем Вы притянули в это обсуждение Perl. Это был, по тем временам, отличный язык. Просто он был не столько про ясный и надёжный код, сколько про самовыражение. Созданный лингвистом, он в этом плане был намного ближе к обычным языкам, чем большинство других языков программирования. И убили его не проблемы самого языка, а проблемы управления - пока развитие языка определялось его автором (вплоть до Perl 5) всё было отлично, но когда он передал руль коммьюнити, то слишком долго (уже более 20 лет) идёт обсуждение новой версии (Perl 6) без выпуска самой этой версии. За столько лет и язык успел заметно устареть, и многие разработчики (включая меня), так и не дождавшись более современного Perl 6, ушли на другие языки. Это проблема из серии "дорога ложка к обеду", а не про то, как всё разваливается из-за недостатка на проекте учёных.
Да (пардон, я пропустил ваш ответ тогда), практическая польза -- очень важное мерило, я с этим согласен. Дисбаланс в наших мнениях, возможно, здесь (цитирую вашу последнюю реплику): "лично меня интересует не процесс и не все подряд результаты, а только те, которые можно применить на практике". Мне процесс и промежуточные результаты инетересны в некоторых областях безотносительно к применению-на-практике-прямо-сейчас. Упражнение ума (изредка всё-таки получается интересные идеи применять на практике самому), плюс -- элемент future proof (ориентироваться в нововведениях заранее).
Практичность, внедрение чего попроще впереди более продуманного с заделом на будущее подхода -- иногда имеет неприятный длинный хвост, опять приведу пример: дженерики в Java. Их ввели в язык с значительной задержкой (возможно, кстати, не без влияния конкурирующего C#, в котором дженерики появились раньше), и получившийся результат не изящен (читаю книгу по Kotlin - там проблему систематически исправляют, но не обходится без заусенцев на стыковках с Java). В момент разработки первой версии языка нужная теория (и практические наработки из других языков) были наготове -- но сделали (правомерно, вероятно) выбор в пользу более раннего релиза более простой, практичной системы без дженериков. То же с Go, я не слежу за ситуацией (вводят там дженерики в новых версиях или нет) -- повторение похожей истории лет 20 после выпуска первой версии Java. С C#/.NET вышло более гладко -- базу для введения более органичный дженериков теоретически разработал (и сделал прототипную реализацию) учёный Don Syme (знаменитый также, как автор и популяризатор F#) -- а стартовали, опять же, без дженериков, "практично".
В Go их не вводили именно потому, что хотели это сделать либо правильно, либо никак - и были готовы годы без них обходиться, пока не появится понимание как же это сделать правильно. В ближайшие недели как раз должна выйти версия с поддержкой дженериков. Пока - несколько урезанной, специально чтобы собрать ещё больше информации о том, нужно ли делать её более навороченной или нет, и как именно её наворачивать если да. Уникальный подход, на самом деле, в современном софте обычно так никто не заморачивается.
Но я Ваш ответ понял, спасибо.
Мы тратим дофига времени переводя эти 2-3 экрана кода в запись, которую можно проверить формально…
Подождите, а зачем переписывать что-то? Модел-чекер, который я описываю, работает с уже готовым кодом на языках поддерживающих компиляцию в llvm. То есть по факту там надо написать ту же строку по типу `go test -race`
О, это уже интересно. Для Go вроде бы есть рабочий компилятор в LLVM https://go.googlesource.com/gollvm. Как будет выглядеть пример использования этого модел-чекера на практике? Допустим, возьмём пример из статьи, напишем на Go, компилируем в LLVM. На выходе в LLVM будет море кода (включая Go-шный рантайм с шедулером горутин, сборщиком мусора, etc.). И вот есть у нас подозрение, что в текущей версии нашего кода есть баг с блокировками. Дальше что нужно делать?
Ну смотрите, конечно, Вам придется один раз немножко поработать, чтоб связать Ваш рантайм и главную процедуру TruSt. В общем случае надо помочь функции next (см выжимку из алгоритма в посте). Но так как это не совсем связано с темой верификации самого алгоритма и является немного оффтопом здесь, я просто дам ссылку на статью в которой это написано https://plv.mpi-sws.org/genmc/cav21-paper.pdf (страница 6). Эта статья про GenMC -- предыдущую версию TruSt, но часть про поддержку языков с компиляцией в llvm не менялась так что, то что там написано остается релевантным.
Если честно не совсем понял Ваш комментарии. Используя TruSt проверка низкоуровневого кода займет как раз не очень много времени и памяти. Так что раз в какой-то момент низкоуровневый код нам придется писать, почему бы не воспользоваться хорошим тулом?
Один из поинтов статьи был как раз в том, что появляются новые методы и с ними то, что раньше на практике были неприменимо совершенствуются и становятся все более и более доступным
И дальше будет "как повезёт". Никаких гарантий отлова состояний гонок race не дает. Кроме того он будет ровно настолько хорош, насколько хороши ваши тесты. И всякие редкие граничные случаи останутся, как правило, жить.
Если надо гарантий, то надо не golang.
Простите, но про вынесенную в заголовок, и самую содержательную \ интересную часть статьи: алгоритм TruSt ничего не написано (к стати и про чекеры моделей - тоже ничего не написано).
Можете в следующих статьях описать?
П.С.
Для примера оставшиеся вопросы:
- Как добились точности (это отсутствие false postitve и false negative ?) вычислительной оптимальности и линейности по памяти?
- Какая она вообще вычислительная оптимальность в этой задаче?
- На коде какой сложности (по числу потоков, ветвлений в потоках) \ размера (понятно, что не очень больших, но каких) алгоритм работает за приемлемое время?
...
Спасибо за Ваш комментарий!
Простите, но про вынесенную в заголовок, и самую содержательную \ интересную часть статьи: алгоритм TruSt ничего не написано
Согласен, в этом плане, может заголовок получился не самым информативным. Однако моей главной задачей было описание верификации данного алгоритма. Остальная информация была дана скорее для того, чтобы было понятно какие конкретно леммы гарантируют корректность алгоритма и как примерно они доказываются.
В этом плане, в основной статье (которая на POPL) про верификацию алгоритма и где конкретно его можно применить написано достаточно мало, так что этот пост скорее надо рассматривать как дополнение к статье, а не попытку перевести ее на русский язык :)
Касательно оставшихся вопросов: все это очень хорошо освещено в основной статье. Но думаю, что если у Вас действительно есть такой запрос, то я могу попробовать, как только будет время, продолжить эту тему (хоть я и не особо вижу смысл в таком дублировании)
PS Я не очень понял чтобы вы хотели услышать про оптимальность? В самом посте описано, что оптимальным алгоритм является, если он не посещает одни и те же графы исполнения несколько раз.
>> Но думаю, что если у Вас действительно есть такой запрос, то я могу попробовать, как только будет время, продолжить эту тему (хоть я и не особо вижу смысл в таком дублировании)
Ну тут сами понимаете: если тяготит - не надо. Если вам интересно написать, думаю найдутся читатели, кому интересно написать.
>> Я не очень понял чтобы вы хотели услышать про оптимальность? В самом посте описано, что оптимальным алгоритм является, если он не посещает одни и те же графы исполнения несколько раз.
Боюсь я вообще ничего не понял начиная вот с этой строчки:a := next(P, G) // выбираем какую инструкцию в программе надо исполнить следующей и записываем соответствующее событие a в G
Какая такая "следующая" инструкция в многопоточном программировании?
Когда сама суть того, что мы проверяем - выполнение констстентности при отсутствии полной упорядоченности инструкций, и отсутствии полной упорядоченности в наблюдаемых эффектах выполнения инструкций.
Какая такая "следующая" инструкция в многопоточном программировании?
Когда сама суть того, что мы проверяем - выполнение констстентности при отсутствии полной упорядоченности инструкций, и отсутствии полной упорядоченности в наблюдаемых эффектах выполнения инструкций.
Отличный вопрос! Если думать о том, что потоки в программе упорядоченны слева направо, то в данном месте проще всего считать что next просто выбирает доступную инструкцию в самом правом потоке.
Первый truly stateless оптимальный алгоритм модел-чекера и его проверка на Coq