pgo
1.0.0
PGO является источником для источника компилятора, который переводит модульные спецификации PlusCal (которые используют Superset of Prolscal) в программы GO.
В дополнение к компилятору PGO, это дерево источника включает в себя:
distsys , которая используется сгенерированным кодом GO PGO, доступна в папке distsys/ .systems/ папке, в том числе хранилище ключей на основе плотов.syntax/ папке.Вы можете прочитать больше об аспектах исследований нашей работы в нашей статье Asplos'23, копия которой включена в этот репозиторий. Наша оценка премии PGO выдающегося артефакта на этой конференции?
У нас также есть пара видео, которые вы можете посмотреть:
Pluscal - это язык для определения/моделирования параллельных систем. Он был разработан, чтобы облегчить писать TLA+. В частности, Pluscal может быть скомпилирован в TLA+, который можно проверить на полезных свойствах системы (с помощью контроля модели TLC). Например, вот репозиторий плюскальных составов решений для проблемы взаимного исключения.
GO - это язык C, разработанный Google для создания распределенных систем. Он встроен в поддержку параллелистики с каналами и Goroutines, что делает его отличным для разработки распределенных систем.
В настоящее время нет никаких инструментов, которые соответствуют спецификации PlusCal/TLA+ с реализацией спецификации. PGO - это инструмент, который направлен на подключение спецификации с реализацией путем генерации кода GO на основе спецификации, записанной в модульной Pluscal. «Модульный» префикс происходит от необходимости отличить описание системы от модели ее среды, которая необходима для проверки моделей. PGO позволяет переводить модульное описание Pluscal распределенной системы в проверку Proscal, а также семантически эквивалентную программу GO.
Активно в процессе развития. PGO поддерживает компиляцию всех конструкций потока управления PlusCal. PGO также поддерживает подавляющее большинство TLA+ уровня стоимости, поддерживаемого TLC. Смотрите запросы на привлечение и проблемы для документации по текущей работе.
В своем состоянии активного развития мы не предоставляем стабильные выпуски. Чтобы запустить PGO, лучший способ - клонировать репозиторий, и, на главной ветви, запустите его через инструмент сборки SBT:
$ sbt
> run [command-line arguments]
См. Примечания к использованию ниже для того, какие аргументы принимают программа. ПРИМЕЧАНИЕ. Если вы запускаете ее на одной строке, то вы должны процитировать аргументы, как в sbt run "[command-line arguments]" .
Чтобы узнать, как использовать PGO во время проверки, см. Страницу использования PGO (предупреждение: обновление в процессе).
Для режимов компиляции инструмента и флагов на высоком уровне см. Ниже.
Справочный текст инструмента PGO читается:
PGo compiler
-h, --help Show help message
Subcommand: gogen
-o, --out-file <arg>
-p, --package-name <arg>
-s, --spec-file <arg>
-h, --help Show help message
Subcommand: pcalgen
-s, --spec-file <arg>
-h, --help Show help message
Подкоманда gogen запрашивает, что PGO генерирует файл GO из MPCAL-содержащего модуля TLA+. Большая часть настройки этого этапа должна быть выполнена путем выбора конкретных параметров при вызове сгенерированного кода GO, поэтому есть только несколько вариантов.
--out-file определяет путь к выходному файлу GO, как -o в GCC.--spec-file определяет путь к входному файлу TLA+--package-name позволяет настройку имени пакета выходного файла GO. Это по умолчанию в дезинфицированную версию названия алгоритма MPCAL. Подкоманда pcalgen требует, чтобы PGO переписывал свой входной файл TLA+, содержащий MPCAL, так что он содержит плюс-перевод алгоритма MPCAL. Единственный вариант, --spec-file ,-это путь к файлу спецификации, который будет переписан.
Чтобы вставить перевод Pluscal, PGO будет искать такие комментарии, как, дайте или принимайте пробелы:
* BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION
Если он не может найти один из этих комментариев в этом порядке, он сдаст сообщение об ошибке, описывающее проблему, и не будет писать никаких выводов.
PGO является источником для источника компилятора, написанного в Scala. Он компилирует спецификации, написанные в расширении Pluscal, называемого Modular Pluscal (см. Модульную страницу Pluscal для получения более подробной информации), чтобы выполнять программы.
Код Scala от PGO строит через проект SBT, с его зависимостями, управляемыми Maven. PGO дополнительно предоставляет библиотеку поддержки времени выполнения для своего сгенерированного кода GO, который живет в distsys/ Subloder. Этот код GO является стандартным модулем GO, который может быть импортирован через URL https://github.com/distcompiler/pgo/distsys.
Основным сценарием сборки является верхний уровень Build.sbt. Чтобы построить из терминала, запустите sbt в корневом каталоге и используйте стандартные команды, предоставленные консолью SBT. Они включают в себя run <command-line args> to (повторно) компилировать и запустить PGO, а также test для запуска всех тестов, включая тесты GO (TODO: добавьте бегуна для отдельных тестов GO; в частности, отсутствует один, отсутствует).
Сборка SBT также может быть автоамированной плагином Intellij Scala, а также, вероятно, любой другой IDE с поддержкой Scala.
Код Scala PGO управлял зависимостью от небольшого набора коммунальных библиотек:
Тестовые наборы PGO дополнительно зависят от:
go исполняемый файл. Тесты попытаются найти это, вероятно, на $PATH или эквивалент, через процесс поиска по умолчанию JVM.Библиотека PGO's Go Runtime зависит от:
PGO тестируется с использованием OpenJDK с 1.11 до 1.16 и GO 1.18. OpenJDK 1.11+ необходим из -за стандартного использования API. GO> = 1,18 необходим из -за дженериков.
