Las propiedades de ejecución, como la terminación, incluso de los programas concurrentes de memoria compartida más sencillos con consistencia secuencial, suelen requerir algunas suposiciones de equidad sobre el programador. En los modelos de memoria débil, las nociones estándar de equidad de los subprocesos no son suficientes y se necesita una propiedad de equidad adicional: la equidad de la memoria. En este proyecto, proponemos definiciones para la equidad de la memoria en los entornos de los modelos de memoria operativa y declarativa como SC, x86-TSO, RA y StrongCOH, e investigamos su uso para la comprobación del modelo y la comprobación de la terminación de los programas concurrentes con sincronización de bajo nivel.

• Repositorio del proyecto