Какая такая "следующая" инструкция в многопоточном программировании? Когда сама суть того, что мы проверяем - выполнение констстентности при отсутствии полной упорядоченности инструкций, и отсутствии полной упорядоченности в наблюдаемых эффектах выполнения инструкций.
Отличный вопрос! Если думать о том, что потоки в программе упорядоченны слева направо, то в данном месте проще всего считать что next просто выбирает доступную инструкцию в самом правом потоке.
Простите, но про вынесенную в заголовок, и самую содержательную \ интересную часть статьи: алгоритм TruSt ничего не написано
Согласен, в этом плане, может заголовок получился не самым информативным. Однако моей главной задачей было описание верификации данного алгоритма. Остальная информация была дана скорее для того, чтобы было понятно какие конкретно леммы гарантируют корректность алгоритма и как примерно они доказываются.
В этом плане, в основной статье (которая на POPL) про верификацию алгоритма и где конкретно его можно применить написано достаточно мало, так что этот пост скорее надо рассматривать как дополнение к статье, а не попытку перевести ее на русский язык :)
Касательно оставшихся вопросов: все это очень хорошо освещено в основной статье. Но думаю, что если у Вас действительно есть такой запрос, то я могу попробовать, как только будет время, продолжить эту тему (хоть я и не особо вижу смысл в таком дублировании)
PS Я не очень понял чтобы вы хотели услышать про оптимальность? В самом посте описано, что оптимальным алгоритм является, если он не посещает одни и те же графы исполнения несколько раз.
Ну смотрите, конечно, Вам придется один раз немножко поработать, чтоб связать Ваш рантайм и главную процедуру TruSt. В общем случае надо помочь функции next (см выжимку из алгоритма в посте). Но так как это не совсем связано с темой верификации самого алгоритма и является немного оффтопом здесь, я просто дам ссылку на статью в которой это написано https://plv.mpi-sws.org/genmc/cav21-paper.pdf (страница 6). Эта статья про GenMC -- предыдущую версию TruSt, но часть про поддержку языков с компиляцией в llvm не менялась так что, то что там написано остается релевантным.
Мы тратим дофига времени переводя эти 2-3 экрана кода в запись, которую можно проверить формально…
Подождите, а зачем переписывать что-то? Модел-чекер, который я описываю, работает с уже готовым кодом на языках поддерживающих компиляцию в llvm. То есть по факту там надо написать ту же строку по типу `go test -race`
Если честно не совсем понял Ваш комментарии. Используя TruSt проверка низкоуровневого кода займет как раз не очень много времени и памяти. Так что раз в какой-то момент низкоуровневый код нам придется писать, почему бы не воспользоваться хорошим тулом?
Один из поинтов статьи был как раз в том, что появляются новые методы и с ними то, что раньше на практике были неприменимо совершенствуются и становятся все более и более доступным
Отличный вопрос! Если думать о том, что потоки в программе упорядоченны слева направо, то в данном месте проще всего считать что
nextпросто выбирает доступную инструкцию в самом правом потоке.Спасибо за Ваш комментарий!
Согласен, в этом плане, может заголовок получился не самым информативным. Однако моей главной задачей было описание верификации данного алгоритма. Остальная информация была дана скорее для того, чтобы было понятно какие конкретно леммы гарантируют корректность алгоритма и как примерно они доказываются.
В этом плане, в основной статье (которая на POPL) про верификацию алгоритма и где конкретно его можно применить написано достаточно мало, так что этот пост скорее надо рассматривать как дополнение к статье, а не попытку перевести ее на русский язык :)
Касательно оставшихся вопросов: все это очень хорошо освещено в основной статье. Но думаю, что если у Вас действительно есть такой запрос, то я могу попробовать, как только будет время, продолжить эту тему (хоть я и не особо вижу смысл в таком дублировании)
PS Я не очень понял чтобы вы хотели услышать про оптимальность? В самом посте описано, что оптимальным алгоритм является, если он не посещает одни и те же графы исполнения несколько раз.
Ну смотрите, конечно, Вам придется один раз немножко поработать, чтоб связать Ваш рантайм и главную процедуру TruSt. В общем случае надо помочь функции
next(см выжимку из алгоритма в посте). Но так как это не совсем связано с темой верификации самого алгоритма и является немного оффтопом здесь, я просто дам ссылку на статью в которой это написано https://plv.mpi-sws.org/genmc/cav21-paper.pdf (страница 6). Эта статья про GenMC -- предыдущую версию TruSt, но часть про поддержку языков с компиляцией в llvm не менялась так что, то что там написано остается релевантным.Подождите, а зачем переписывать что-то? Модел-чекер, который я описываю, работает с уже готовым кодом на языках поддерживающих компиляцию в llvm. То есть по факту там надо написать ту же строку по типу `go test -race`
Если честно не совсем понял Ваш комментарии. Используя TruSt проверка низкоуровневого кода займет как раз не очень много времени и памяти. Так что раз в какой-то момент низкоуровневый код нам придется писать, почему бы не воспользоваться хорошим тулом?
Один из поинтов статьи был как раз в том, что появляются новые методы и с ними то, что раньше на практике были неприменимо совершенствуются и становятся все более и более доступным