Generación de invariantes para implementar eficientemente regiones críticas condicionales

Abstract

La técnica de semáforos binarios divididos (SBS) puede ser usada para implementar regiones críticas condicionales. Dada una especificación de un problema de esta clase. SBS brinda tanto los programas que lo implementan como los invariantes que aseguran su corrección. Aplicando la técnica a casos particulares se encuentran programas que admiten simplificaciones. Este trabajo se concentra en el desarrollo de un sistema automático para obtener estas simplificaciones. El procedimiento consiste en hacer una búsqueda de nuevos invariantes que avalen la corrección de las simplificaciones. Para esto usamos técnicas de generación de invariantes, en particular propagación hacia los más débiles. Su implementación fue realizada usando los demostradores Isabelle /HOL v CVC Lite para las demostraciones de validez y simplificaciones de las formulas lógicas envueltas en el proceso. El método fue probado sobre diferentes ejemplos clásicos de programación concurrente.