pgoダウンロードpgoソースコードのダウンロード

pgo

その他のソースコード

1.0.0

ダウンロード

PGO

PGOは、Modular PlusCal仕様（PlusCalのスーパーセットを使用）をGOプログラムに変換するソースコンパイラのソースです。

PGOコンパイラに加えて、このソースツリーには以下が含まれます。

distsysサポートライブラリは、PGOの生成されたGOコードで使用されており、 distsys/ Folderで使用できます。
ラフトベースのキー値ストアを含む、 systems/フォルダー内のPGOを使用して構築されたシステム。
syntax/フォルダーで使用できる、Visual Studio Code and Pygmentsのモードを強調表示します。

私たちの作品の研究の側面については、Asplos'23論文で詳細を読むことができます。そのコピーはこのリポジトリに含まれています。その会議でのPGO特別アーティファクト賞の評価？

また、見ることができるビデオもいくつかあります。

PGO TLA+ Conference Talk、2022年9月
PGOの概要講演、2022年2月。

目的と動機

PlusCalは、同時システムを指定/モデリングするための言語です。 TLA+を簡単に記述できるように設計されています。特に、PlusCalはTLA+にコンパイルできます。TLA+は、有用なシステムプロパティ（TLCモデルチェッカーを使用）に対して確認できます。たとえば、ここに相互排除問題に対するソリューションのプラスカル定式化のリポジトリがあります。

GOは、分散システムを構築するためにGoogleが開発したCベースの言語です。チャネルとの並行性とゴルチンをサポートしているため、分散システムの開発に最適です。

現在、スペックの実装を使用してPlusCal/TLA+仕様に対応するツールはありません。 PGOは、Modular PlusCalで記述された仕様に基づいてGOコードを生成することにより、仕様を実装と接続することを目的とするツールです。「モジュラー」プレフィックスは、システムの説明を環境のモデルと区別する必要性から生じます。これは、モデルチェックに必要です。 PGOは、分散システムのモジュラープラスカルの説明の検証可能なプラスカル、および意味的に同等のGOプログラムへの翻訳を可能にします。

現在のステータス

積極的に開発中。 PGOは、すべてのプラスカル制御フローコンストラクトの編集をサポートしています。 PGOはまた、TLCによってサポートされる価値レベルのTLA+の大部分をサポートしています。進行中の作業のドキュメントについては、プルリクエストと問題を参照してください。

アクティブ開発状態では、安定したリリースは提供しません。 PGOを実行するには、最良の方法はリポジトリをクローン化し、マスターブランチでSBTビルドツールを介して実行することです。

 $ sbt
> run [command-line arguments]

プログラムが受け入れる議論については、以下の使用法を参照してください。注：1行で実行する場合は、 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 GCCの-oのように、GO出力ファイルへのパスを指定します。
--spec-file TLA+入力ファイルへのパスを指定します
--package-nameと、Go Outputファイルのパッケージ名をカスタマイズできます。これにより、MPCALアルゴリズム名の消毒版がデフォルトです。

pcalgen

pcalgenサブコマンドは、MPCALアルゴリズムのプラスカル翻訳が含まれるように、PGOがMPCALを含むTLA+入力ファイルを書き換えるように要求します。唯一のオプション、 --spec-file 、書き換えられる仕様ファイルへのパスです。

PlusCalの翻訳を挿入するには、PGOはWhitespaceなどのコメントを探します。

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

これらのコメントの両方の1つがその順序で見つからない場合、問題を説明するエラーメッセージをあきらめ、出力を書き込みません。

それがどのように機能するか

PGOは、Scalaで書かれたソースコンパイラのソースです。 Modular PlusCalと呼ばれるPlusCalの拡張機能で記述された仕様をコンパイルします（詳細については、Modular PlusCalページを参照）、GOプログラムを作成します。

構築方法（開発のため）

PGOのSCALAコードは、Mavenが管理する依存関係により、SBTプロジェクトを介して構築されます。 PGOは、 distsys/ Subfolderに住んでいる生成されたGOコードのランタイムサポートライブラリをさらに提供します。このGOコードは標準のGOモジュールであり、URL https://github.com/distcompiler/pgo/distsysを介してインポートできます。

メインビルドスクリプトは、トップレベルのbuild.sbtです。ターミナルから構築するには、ルートディレクトリでsbt実行し、SBTコンソールが提供する標準コマンドを使用します。これらには、 run <command-line args> to（re）コンパイルおよびPGOを実行すること、およびGOテストを含むすべてのテストを実行するためのtestが含まれます（TODO：フリースタンディングGOテストのランナーを追加します。具体的には欠落しています）。

SBTビルドは、Intellij Scalaプラグインによって自動インポートすることもできます。また、SCALAサポートを備えた他のIDEも可能です。

PGOのSCALAコードは、ユーティリティライブラリの小さなセットで依存関係を管理しています。