pgo
1.0.0
PGO es una fuente para el compilador de origen que traduce las especificaciones modulares de Pluscal (que usan un superset of Pluscal) en los programas GO.
Además del compilador PGO, este árbol de origen incluye:
distsys , que utiliza el código GO generado por PGO, disponible en la carpeta distsys/ .systems/ carpeta, incluida una tienda de valores clave basada en balsa.syntax/ carpeta.Puede leer más sobre los aspectos de investigación de nuestro trabajo en nuestro documento ASPlos'23, una copia de la cual se incluye en este repositorio. ¿Nuestra evaluación del premio de artefacto distinguido de PGO en esa conferencia?
También tenemos un par de videos que puedes ver:
Pluscal es un idioma para especificar/modelar sistemas concurrentes. Fue diseñado para facilitar la escritura TLA+. En particular, Pluscal se puede compilar en TLA+, que se puede verificar en propiedades útiles del sistema (utilizando el revisor del modelo TLC). Por ejemplo, aquí hay un repositorio de formulaciones máscales de soluciones al problema de exclusión mutua.
GO es un lenguaje basado en C desarrollado por Google para construir sistemas distribuidos. Tiene soporte incorporado para la concurrencia con canales y goroutinas, lo que lo hace excelente para desarrollar sistemas distribuidos.
Actualmente no hay herramientas que correspondan una especificación de Pluscal/TLA+ con una implementación de la especificación. PGO es una herramienta que tiene como objetivo conectar la especificación con la implementación generando el código GO basado en una especificación escrita en Modular Pluscal. El prefijo "modular" proviene de la necesidad de distinguir la descripción de un sistema del modelo de su entorno, que es necesario para la verificación del modelo. PGO permite la traducción de una descripción modular de Pluscal de un sistema distribuido a verificable Pluscal, así como a un programa GO semánticamente equivalente.
Activamente en desarrollo. PGO admite la compilación de todas las construcciones de flujo de control más pluscal. PGO también admite una gran mayoría de los TLA de nivel de valor respaldado por TLC. Consulte las solicitudes de extracción y los problemas para la documentación del trabajo en curso.
En su estado de desarrollo activo, no proporcionamos lanzamientos estables. Para ejecutar PGO, la mejor manera es clonar el repositorio y, en la rama maestra, ejecutarlo a través de la herramienta de compilación SBT:
$ sbt
> run [command-line arguments]
Consulte las notas de uso a continuación para obtener qué argumentos acepta el programa. Nota: Si lo ejecuta en una línea, entonces debe citar los argumentos, como en sbt run "[command-line arguments]" .
Para aprender a usar PGO durante la verificación, consulte la página de uso de PGO (Advertencia: Actualización en progreso).
Para los modos y banderas de compilación de la herramienta en un nivel alto, consulte a continuación.
El texto de ayuda de la herramienta PGO dice:
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
El subcomando gogen solicita que PGO genere un archivo GO a partir de un módulo TLA+ que contiene MPCAL. La mayoría de la personalización de esta etapa debe hacerse eligiendo parámetros específicos al llamar al código GO generado, por lo que solo hay algunas opciones a considerar.
--out-file especifica la ruta al archivo de salida GO, como -o en GCC.--spec-file especifica la ruta al archivo de entrada TLA+--package-name permite la personalización del nombre del paquete del archivo de salida GO. Esto es predeterminado a una versión desinfectada del nombre del algoritmo MPCAL. El subcomando pcalgen solicita que PGO reescribe su archivo de entrada TLA+ que contiene MPCAL, de modo que contiene una traducción máscal del algoritmo MPCAL. La única opción, --spec-file , es la ruta al archivo de especificaciones, que se reescribirá.
Para insertar la traducción de Pluscal, PGO buscará comentarios como, dar o tomar espacios en blanco:
* BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION
Si no puede encontrar uno de ambos comentarios en ese orden, renunciará a un mensaje de error que describe el problema y no escribirá ningún resultado.
PGO es una fuente para el compilador de origen escrito en Scala. Compila especificaciones escritas en una extensión de Pluscal, llamada Modular Pluscal (consulte la página Modular Pluscal para obtener más detalles), para los programas GO.
El código SCALA de PGO se construye a través de un proyecto SBT, con sus dependencias administradas por Maven. PGO también proporciona una biblioteca de soporte de tiempo de ejecución para su código GO generado, que vive en distsys/ subcarpeta. Este código GO es un módulo GO estándar, que se puede importar a través de la URL https://github.com/distcompiler/pgo/distsys.
El script de compilación principal es el build.sbt de nivel superior. Para construir desde el terminal, ejecute sbt en el directorio raíz y use los comandos estándar proporcionados por la consola SBT. Estos incluyen run <command-line args> para (re) compilar y ejecutar PGO, y test para ejecutar todas las pruebas, incluidas las pruebas GO (TODO: Agregar corredor para pruebas GO independientes; esa, específicamente, falta).
La construcción SBT también puede ser automática por el complemento IntelliJ Scala, así como probablemente cualquier otro IDE con soporte de Scala.
El código SCALA de PGO ha administrado dependencias en un pequeño conjunto de bibliotecas de servicios públicos:
Las suites de prueba de PGO también dependen de:
go ejecutable. Las pruebas intentarán encontrar esto, probablemente en la $PATH o equivalente, a través del proceso de búsqueda predeterminado del JVM.La biblioteca de tiempo de ejecución de PGO GO depende de:
El PGO se prueba utilizando OpenJDK 1.11 a 1.16, y Go 1.18. Se necesita OpenJDK 1.11+ debido al uso estándar de API. GO> = 1.18 es necesario debido a los genéricos.
