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是由於仿製藥而需要的。