Fully abstract trace semantics for protected module architectures
Formalises A+I A + I : an assembly language extended with protected module architectures  an isolation mechanism found in emerging processors. Presents two trace semantics for A+I A + I programs and proves that both are fully abstract w.r.t. the operational semantics. Details which problems arise when considering readout and writeout labels in the trace semantics of A+I A + I programs.
trace semantics protected modules architectures fully abstract semantics untyped assembly language formal languages