Verificación modular de atomicidad en bytecode Java Multi-Thread

Abstract

En este trabajo se presenta una técnica para verificar modularmente atomicidad de programas bytecode Java multi-thread. Los programas deben contar con una especificación referente a los bloqueos y al acceso a los recursos compartidos para realizar la verificación modular. Se presenta la compilación propuesta de programas fuente Java con la especificación de atomicidad a bytecode Java, con dichas especificaciones incluidas el código compilado. Garantizar atomicidad en programas mult-thread permite, posteriormente, verificar propiedades funcionales más complejas utilizando técnicas para programas secuenciales.