Sail and Isla ecosystems

Sailor depends on a useful shift in how hardware behavior is described: architecture specifications can be written as executable models rather than only as prose. Sail is a language for writing those ISA models, so the semantics of registers, instructions, and privilege behavior can be inspected by tools.

Isla complements that by symbolically executing Sail models. Instead of running one concrete instruction instance, symbolic execution can explore how instruction behavior depends on conditions and state. For context switching, that matters because the question is not just which state is visible, but which state can be read or modified by the ISA under relevant execution paths.

This separation is powerful. Sail captures architectural intent, Isla collects behavior from that model, and Sailor asks a security-specific question over the collected data: what must a context switch preserve so that one context cannot inherit, corrupt, or learn state from another?

The result is a workflow that scales better than hand-reading ISA manuals. As architectures evolve and extensions add state, the same ecosystem can be reused to re-check whether privileged software still saves what must be saved.