pgo 다운로드 pgo 소스 코드 다운로드

pgo

기타 소스코드

1.0.0

다운로드

PGO

PGO는 모듈 식 플러스 칼 사양 (PlusCal의 슈퍼 세트를 사용하는)을 GO 프로그램으로 변환하는 소스 소스 컴파일러입니다.

PGO 컴파일러 외에도이 소스 트리에는 다음이 포함됩니다.

PGO의 생성 된 GO 코드에서 사용하는 distsys Support Library는 distsys/ Folder에서 사용할 수 있습니다.
뗏목 기반 키 값 저장소를 포함하여 systems/ 폴더에서 PGO를 사용하여 구축 된 시스템.
syntax/ 폴더에서 사용할 수있는 Visual Studio Code 및 Pygments의 구문 강조 표시 모드.

ASPLOS'23 논문의 연구 측면에 대한 자세한 내용은이 저장소에 포함되어 있습니다. 그 회의에서 PGO Distinguished Artifact Award에 대한 우리의 평가는?.

또한 볼 수있는 몇 가지 비디오도 있습니다.

PGO TLA+ 컨퍼런스 토크, 2022 년 9 월
PGO 개요 토크, 2022 년 2 월.

목적과 동기 부여

Pluscal은 동시 시스템을 지정/모델링하는 언어입니다. TLA+를 더 쉽게 작성할 수 있도록 설계되었습니다. 특히, PlusCal은 TLA+로 컴파일 될 수 있으며, 이는 유용한 시스템 속성 (TLC 모델 체커 사용)에 대해 확인할 수 있습니다. 예를 들어, 여기에는 상호 배제 문제에 대한 솔루션의 플러스 칼 공식 저장소가 있습니다.

GO는 Google이 분산 시스템을 구축하기 위해 개발 한 C 기반 언어입니다. 채널과 동시성을 지원하고 Goroutines를 지원하여 분산 시스템을 개발하는 데 좋습니다.

현재 PlusCal/TLA+ 사양에 해당하는 도구는 사양의 구현으로 없습니다. PGO는 Modular PlusCal로 작성된 사양을 기반으로 GO 코드를 생성하여 사양을 구현에 연결하는 도구입니다. "모듈 식"접두사는 시스템의 모델과 모델 점검에 필요한 환경 모델과 구별해야 할 필요성에서 비롯됩니다. PGO는 분산 시스템의 모듈 식 플러스 칼 설명을 검증 가능한 플러스 칼로 및 의미 적으로 동등한 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

gogen 하위 명령은 PGO가 MPCAL 함유 TLA+ 모듈에서 GO 파일을 생성하도록 요청합니다. 이 단계의 대부분의 사용자 정의는 생성 된 GO 코드를 호출 할 때 특정 매개 변수를 선택하여 수행해야하므로 고려해야 할 몇 가지 옵션 만 있습니다.

--out-file GCC의 -o 와 같은 GO 출력 파일의 경로를 지정합니다.
--spec-file tla+ 입력 파일의 경로를 지정합니다
--package-name GO 출력 파일의 패키지 이름을 사용자 정의 할 수 있습니다. 이 기본값은 MPCAL 알고리즘 이름의 소독된 버전으로 변합니다.

pcalgen

pcalgen 하위 명령은 PGO가 MPCAL 함유 TLA+ 입력 파일을 다시 작성하여 MPCAL 알고리즘의 플러스 칼 번역을 포함하도록 요청합니다. 유일한 옵션 인 --spec-file 사양 파일의 경로이며 다시 작성됩니다.

PlusCal Translation을 삽입하려면 PGO는 whitespace, Give 또는 Take와 같은 의견을 찾습니다.

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

이 두 의견 중 하나를 순서대로 찾을 수 없다면 문제를 설명하는 오류 메시지를 포기하고 출력을 작성하지 않습니다.

작동 방식

PGO는 Scala로 작성된 소스 컴파일러 소스입니다. GO 프로그램을 위해 Modular PlusCal (Modular PlusCal 페이지 참조)이라고하는 PlusCal의 확장으로 작성된 사양을 컴파일합니다.

구축 방법 (개발 용)

PGO의 Scala Code는 SBT 프로젝트를 통해 Maven이 관리하는 종속성을 통해 구축됩니다. PGO는 distsys/ Subfolder에 살고있는 생성 된 GO 코드에 대한 런타임 지원 라이브러리를 추가로 제공합니다. 이 GO 코드는 표준 GO 모듈로 URL https://github.com/distcompiler/pgo/distsys를 통해 가져올 수 있습니다.

메인 빌드 스크립트는 최상위 빌드입니다. 터미널에서 빌드하려면 루트 디렉토리에서 sbt 실행하고 SBT 콘솔에서 제공하는 표준 명령을 사용하십시오. 여기에는 run <command-line args> to (re) 컴파일 및 실행 PGO가 포함되며, GO 테스트를 포함한 모든 테스트를 실행하기위한 test (TODO : 프리 스탠딩 GO 테스트를위한 러너 추가, 특히 하나, 특히 누락되었습니다).

SBT 빌드는 또한 Intellij Scala 플러그인에 의해 자동 절제 될 수 있으며 스칼라 지원을 통한 다른 IDE 가능성이 있습니다.

PGO의 Scala Code는 작은 유틸리티 라이브러리 세트에 대한 종속성을 관리했습니다.

명령 줄 인수 구문 분석을위한 가리비
TLA+/PCAL/MPCAL 파서에 대한 Scala-Parser-Combinator
단순화 된 파일 및 프로세스 조작을위한 OS-LIB (테스트 중에 프로세스 조작이 사용됨)

PGO의 테스트 스위트는 다음에 추가로 의존합니다.

go 실행 파일. 테스트는 아마도 JVM의 기본 조회 프로세스를 통해 아마도 $PATH 또는 동등한 상태에서 이것을 찾으려고 시도합니다.
테스트 프레임 워크로서의 Scalatest
퍼즈 테스트 구현을위한 Scalacheck
테스트가 큰 텍스트 블록을 비교할 때 차이를 생성하기위한 Java-diff-utils

PGO의 GO 런타임 라이브러리는 다음에 따라 다릅니다.