pgo
1.0.0
O PGO é um compilador de origem para origem que traduz as especificações Modulares PlusCal (que usam um superconjunto do PlusCal) nos programas Go.
Além do compilador PGO, esta árvore de origem inclui:
distsys , usada pelo código GO gerado pelo PGO, disponível na pasta distsys/ .systems/ pasta, incluindo uma loja de valor de chave baseada em jangada.syntax/ pasta.Você pode ler mais sobre os aspectos de pesquisa de nosso trabalho em nosso artigo ASPLOS'23, cuja cópia está incluída neste repositório. Nossa avaliação do prêmio de artefato Distinguished PGO nessa conferência?
Também temos alguns vídeos que você pode assistir:
O Pluscal é um idioma para especificar/modelar sistemas simultâneos. Foi projetado para facilitar a redação do TLA+. Em particular, o PlusCal pode ser compilado no TLA+, que pode ser verificado em relação às propriedades úteis do sistema (usando o verificador de modelo TLC). Por exemplo, aqui está um repositório de formulações positivas de soluções para o problema de exclusão mútua.
GO é uma linguagem baseada em C desenvolvida pelo Google para construir sistemas distribuídos. Ele construiu suporte para simultaneidade com canais e goroutines, o que o torna ótimo para o desenvolvimento de sistemas distribuídos.
Atualmente, não existem ferramentas que correspondam a uma especificação PlusCal/TLA+ com uma implementação da especificação. O PGO é uma ferramenta que visa conectar a especificação com a implementação, gerando código GO com base em uma especificação escrita no Modular Pluscal. O prefixo "modular" vem da necessidade de distinguir a descrição de um sistema do modelo de seu ambiente, necessário para a verificação do modelo. O PGO permite a tradução de uma descrição Modular Pluscal de um sistema distribuído para verificável PlusCal, bem como para um programa GO semanticamente equivalente.
Ativamente em desenvolvimento. O PGO suporta a compilação de todas as construções de fluxo de controle Pluscal. O PGO também suporta uma grande maioria do TLA+ de nível de valor suportado pelo TLC. Consulte as solicitações de tração e problemas para documentação do trabalho em andamento.
Em seu estado de desenvolvimento ativo, não fornecemos lançamentos estáveis. Para executar o PGO, a melhor maneira é clonar o repositório e, no ramo mestre, executá -lo através da ferramenta SBT Build:
$ sbt
> run [command-line arguments]
Veja as notas de uso abaixo para quais argumentos o programa aceita. Nota: Se você o executar em uma linha, deverá citar os argumentos, como no sbt run "[command-line arguments]" .
Para aprender a usar o PGO durante a verificação, consulte a página de uso do PGO (aviso: atualização em andamento).
Para os modos e sinalizadores de compilação da ferramenta em um nível alto, veja abaixo.
O texto de ajuda da ferramenta PGO diz:
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
O subcomando gogen solicita que o PGO gerem um arquivo GO de um módulo TLA+ contendo MPCAL. A maior parte desse estágio deve ser feita escolhendo parâmetros específicos ao chamar o código GO GERADO, para que haja apenas algumas opções a serem consideradas.
--out-file especifica o caminho para o arquivo de saída GO, como -o no GCC.--spec-file especifica o caminho para o arquivo de entrada TLA+--package-name permite a personalização do nome do pacote do arquivo de saída GO. Isso padrão é uma versão higienizada do nome do algoritmo MPCAL. O Subcomando pcalgen solicita que o PGO reescreva seu arquivo de entrada TLA+ contendo MPCAL, de modo que ele contém uma tradução Pluscal do algoritmo MPCAL. A única opção, --spec-file , é o caminho para o arquivo de especificações, que será reescrito.
Para inserir a tradução Pluscal, o PGO procurará comentários como, dê ou aceite o espaço em branco:
* BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION
Se não conseguir encontrar um desses dois comentários nessa ordem, desistirá de uma mensagem de erro descrevendo o problema e não gravará nenhuma saída.
O PGO é uma fonte para o compilador de origem escrito em Scala. Ele compila especificações escritas em uma extensão do Pluscal, chamado Modular Pluscal (consulte a página Modular Pluscal para obter mais detalhes), para ir programas.
O código Scala da PGO é criado através de um projeto SBT, com suas dependências gerenciadas pelo Maven. Além disso, o PGO fornece uma biblioteca de suporte de tempo de execução para o seu código Gerado, que vive na distsys/ subpasta. Esse código GO é um módulo GO padrão, que pode ser importado através do URL https://github.com/distcompiler/pgo/distsys.
O script principal de construção é a compilação de nível superior. Para construir a partir do terminal, execute sbt no diretório raiz e use os comandos padrão fornecidos pelo console SBT. Isso inclui run <command-line args> para (re-) compilar e executar o PGO e test para executar todos os testes, incluindo testes GO (TODO: Adicionar corredor para testes GO independentes; esse, especificamente, está faltando).
A compilação SBT também pode ser implementada automaticamente pelo plug-in Intellij Scala, além de provavelmente qualquer outro IDE com suporte de Scala.
O Código Scala da PGO gerenciou dependências em um pequeno conjunto de bibliotecas de serviços públicos:
As suítes de teste da PGO dependem adicionalmente de:
go executável. Os testes tentarão encontrar isso, provavelmente no $PATH ou equivalente, através do processo de pesquisa padrão da JVM.A biblioteca Go RunTime da PGO depende de:
O PGO é testado usando o OpenJDK 1.11 a 1.16 e vá 1,18. OpenJDK 1.11+ é necessário devido ao uso padrão da API. GO> = 1,18 é necessário por causa dos genéricos.
