pgo

PGO

PGO是源编译器的来源，该编译器将模块化加上规格（使用加号超集）转换为GO程序。

除了PGO编译器外，此源树还包括：

• distsys支持库，该库由PGO生成的GO代码使用，可在distsys/文件夹中使用。
• 在systems/文件夹中使用PGO构建的系统，包括基于筏的钥匙值商店。
• 语法突出显示了Visual Studio代码和Pygments的模式，在syntax/文件夹中可用。

您可以在Asplos'23论文中阅读有关我们作品的研究方面的更多信息，该论文中包含该副本的副本。我们在该会议上对PGO杰出人工制品奖的评估？

我们还可以观看几个视频：

• PGO TLA+会议演讲，2022年9月
• PGO概述谈话，2022年2月。

目的和动力

PlusCal是一种用于指定/建模并发系统的语言。它旨在使编写TLA+更容易。特别是，可以将PlusCal编译到TLA+中，可以根据有用的系统属性（使用TLC型号检查器）进行检查。例如，这里是相互排除问题解决方案的加法公式的存储库。

GO是Google开发的基于C的语言，用于构建分布式系统。它构建了支持与渠道和goroutines并发的支持，这非常适合开发分布式系统。

当前，没有工具可以与规格的实现相通用加上/TLA+规格。 PGO是一种工具，旨在通过基于模块化加号编写的规范生成GO代码来将规范与实现联系起来。 “模块化”前缀源于需要将系统的描述与其环境模型区分开，这是模型检查所需的。 PGO启用了分布式系统的模块化加法描述为可验证加上cal以及语义上等效的GO程序的翻译。

当前状态

积极发展。 PGO支持所有加上控制流构建体的汇编。 PGO还支持TLC支持的绝大多数值级TLA+。有关正在进行的工作的文档，请参阅拉的请求和问题。

在其积极发展状态下，我们不提供稳定的版本。要运行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从含MPCAL的TLA+模块生成GO文件。此阶段的大多数自定义应通过在调用生成的GO代码时选择特定参数来完成，因此只有几个选项要考虑。

• --out-file指定GO输出文件的路径，例如GCC中的-o 。
• --spec-file指定TLA+输入文件的路径
• --package-name允许自定义GO输出文件的软件包名称。这默认为MPCAL算法名称的消毒版本。

PCALGEN

pcalgen子命令请求PGO重写其含MPCAL的TLA+输入文件，以便它包含MPCAL算法的加上转换。唯一的选项--spec-file是将重写SPEC文件的路径。

为了插入加法翻译，PGO将寻找诸如，给或采用Whitespace之类的评论：

 * BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION

如果它找不到以该顺序找到这两个注释的一个，它将放弃描述问题的错误消息，并且不会写任何输出。

它如何工作

PGO是用Scala编写的源编译器的来源。它编译了以PlusCal的扩展为“模块化PlusCal”（有关更多详细信息，请参见模块化PlusCal）的规格。

如何建立（开发）

PGO的Scala代码通过SBT项目构建，其依赖关系由Maven管理。 PGO还为其生成的GO代码提供了一个运行时支持库，该代码居住在distsys/ subfolter中。此GO代码是标准GO模块，可以通过url https://github.com/distcompiler/pgo/dissys导入。

主要的构建脚本是顶级构建。要从终端构建，请在根目录中运行sbt并使用SBT控制台提供的标准命令。其中包括run <command-line args> to（重新）编译和运行PGO，并test以运行所有测试，包括GO测试（TODO：添加Runner以进行独立的GO测试；尤其是丢失的测试）。

SBT构建也可以由Intellij Scala插件自动构成，并且可能具有Scala支持的任何其他IDE。

PGO的Scala代码已管理对一小部分公用事业库的依赖性：

• 命令行参数解析的扇贝
• TLA+/PCAL/MPCAL解析器的Scala-Parser-Comminator
• 用于简化文件和过程操作的OS-LIB（在测试期间使用过程操作）

PGO的测试套件还取决于：

• go执行。这些测试将尝试通过JVM的默认查找过程在$PATH或同等学历上找到它。
• Scalatest作为测试框架
• 用于实施模糊测试的Scalacheck
• 当测试比较大型文本时，用于生成差异的Java-Diff-Utils

PGO的GO运行时库取决于：

• 不可变化，可在TLA+数据模型中有效地实现列表和地图的实现。例如，创建具有一个不同键值对的修改图应花费恒定时间，而不是复制整个现有结构。
• Multierr用于组合错误。

使用OpenJDK 1.11至1.16测试PGO，然后进行1.18。由于标准API使用情况，需要OpenJDK 1.11+。 GO> = 1.18是由于仿制药而需要的。