1 Testing Composable SpecificationsKen McMillan Microsoft Research

2 Case study TileLink is a protocol for implementing a coherent memory in a system-on-chip (SoC). Goal: a formal, modular specification of TileLink Specify the protocol Prove that it implements correct memory semantics Rigorously test component implementations Allow rapid configuration of SoC designs

3 TileLink system Hierarchy of memory system components for SoC using a common interface protocol. TL CORE L2$ NET DIR MEM Hierarchy implements weakly consistent memory model.

4 Modular verification General approach: Composable specifications:Write generic formal specifications of components Verify components locally against specifications Infer that systems of such components are correct Composable specifications: Correctness of components implies correctness of system. With a composable specification, we can assemble arbitrary configurations of components. Some composable specifications are better than others, however…

5 Good composability Assume/guarantee specificationsA conjunction of temporal properties of interfaces Assume/guarantee relationships A B 𝑝 A: “𝐺 (𝐻𝑞⇒𝑝)” B: “𝐺 (𝐻𝑝⇒𝑞)” A∥B: “𝐺(𝑝∧𝑞)” composable! 𝑞 This proof is checkable in P-time We want our specifications to be composable “by construction”.

6 Memory semantics op(loc,kind,addr,data) Memory operations: CPUread write atomic Happens-before relation on operations: happens-before(𝑜 𝑝 1 ,𝑜 𝑝 2 ) ⇔ loc(𝑜 𝑝 1 ) = loc(𝑜 𝑝 2 ) ∧ time(𝑜 𝑝 1 ) < time(𝑜 𝑝 2 ) ∧ (addr(𝑜 𝑝 1 ) = addr(𝑜 𝑝 2 ) ∨ atomic(𝑜 𝑝 1 ) ∨ atomic(𝑜 𝑝 2 )) Consistency: A sequence of ops is consistency if every read sees value of most recent write. Weak consistency: A set of operations is weakly consistent if there exists an ordering 𝜋 s.t: 𝜋 respects happens-before 𝜋 is consistent

7 Problem How do you write a “good” composable specification for a system if its key property refers to all events in the system? How do we witness the serialization 𝜋? How do local operations fit into the global serialization?

8 Solution Add a “reference object”. Constructs the witness for 𝜋.Verifies consistency 𝜋 as it is constructed ref. create commit create : op × loc → stamp commit : stamp → unit eval : stamp → value eval mem commit(stamp): assumes happens-before(X,op(stamp)) ⇒ committed(X) value = eval(stamp): guarantees value = result(𝜋,op(stamp)) assumes committed(stamp) These operations allow us to define the semantics of the system interfaces.

9 TileLink system Hierarchy of memory system components for SoC using a common interface protocol. TL CORE L2$ NET DIR MEM

10 TileLink interface protocolProtocol messages implement Coherent requests (MESI) Invalidation Ordered, non-coherent operations Interface has two roles: Client ≈ processor Manager ≈ memory client manager Typical transaction flow at interface Acquire Grants Finish Probe Release

11 Writing a “good” composable specSpecification has two parts: Temporal properties of interface Assume/guarantee relationships between properties Interface properties of two types: Interface protocol properties Semantic properties, relative to reference object

12 Semantic interface propertiesThese properties refer to the reference object to define ordering and data values at the interface. Manager-side properties M[1]: Data in cached Grant must match ref.mem. M[2]: If uncached resp. then committed(stamp) M[3]: If uncached resp. then data = eval(stamp) Client-side properties C[1]: Data in cached Release must match ref.mem. C[2]: If uncached req. then happens-before(X,stamp) implies requested(X). C[3]: If uncached resp. then data = eval(stamp)

13 Commitment propertiesThe coherence state determines what commitments are allowed on either side of the interface. This is the function of coherence. Client-side commitments: SC[1]: Read may be committed on client side only if interface has shared or exclusive permissions. SC[2]: Write may be committed on client side only if interface has exclusive permissions. Manager-side properties SM[1]: Read may be committed on manager side only if interface has shared or invalid permissions. SM[2]: Write may be committed on manager side only if interface has invalid permissions. Note: “client side” means any component left of the interface.

14 Assume/guarantee relationshipsAn L2 cache has TileLink interfaces on processor side and memory side. 𝐶 𝑚 𝑀 𝑐 𝑴 𝒎 𝑪 𝒄 … 𝑐𝑜𝑚𝑝 𝑃 … 𝑐𝑜𝑚𝑝 𝑺𝑴 𝒎 𝑆𝑀 𝑐 reference object 𝑆𝐶 𝑚 𝑺𝑪 𝒄 𝑹 𝑨 𝑷

15 Assume/guarantee relationshipsAn L2 cache has TileLink interfaces on processor side and memory side. 𝐶 𝑚 𝑀 𝑐 𝑴 𝒎 𝑪 𝒄 … 𝑐𝑜𝑚𝑝 𝑃 … 𝑐𝑜𝑚𝑝 𝑺𝑴 𝒎 𝑆𝑀 𝑐 reference object 𝑆𝐶 𝑚 𝑺𝑪 𝒄 𝑹 𝑨 𝑷 P,R: 𝐶 𝑚 − , 𝑀 𝑐 − → 𝐶 𝑐 , 𝑀 𝑚 P,R: 𝑆 𝐶 𝑚 , 𝐶 𝑚 − , 𝑀 𝑐 − → 𝑆 𝐶 𝑐 P,R: 𝑆 𝑀 𝑐 , 𝐶 𝑚 − , 𝑀 𝑐 − → 𝑆 𝑀 𝑚 P,R: 𝐶 𝑚 − , 𝑀 𝑐 − , 𝑆 𝑀 𝑐 − , 𝑆 𝐶 𝑚 − → 𝑅 𝐴 𝑃 Checking this proof is a purely syntactic operation 𝐺 𝑅 𝐴 𝑝

16 Formal proofs We can now formally verify components in isolation against their assume/guarantee specifications: Reording buffer Hierarchical cache Processor, memory, etc. These are simple abstract component models, intended to show that the specification has the intended implementations. Show key property that protocol is insensitive to message re- ordering. In the process, specification was corrected. Because our assume/guarantee specification is composable, we know that hierarchies built from these components implement a weakly consistent shared memory.

17 Compositional testingFrom an assume/guarantee specification, we can automatically generate a test environment. 𝐶 𝑚 𝑀 𝑐 𝑆𝐶 𝑚 𝑆𝑀 𝑐 𝑴 𝒎 𝑪 𝒄 𝑺𝑴 𝒎 𝑺𝑪 𝒄 … 𝑐𝑜𝑚𝑝 check 𝐿2 RTL generate reference object check 𝑹 𝑨 𝑷 Tested two RTL level components with randomized generation using Z3: L2 cache bank Snooping hub

18 Testing results Compositional testing revealed currency errors in the RTL in under 1s (< 100 cycles) Unit testing provides much greater flexibility in covering internal corner cases Randomized specification-based testing reduces bias Latent bugs Most bugs could not be stimulated in integration test Latent bugs affect re-usability Importance of composability All system-level errors exposed to unit testing Gain confidence that components can be assembled into arbitrary configuration.

19 Conclusion Good composable specification is such that:Correct component imply correct system The proof of this is efficiently checkable Global properties (such as memory consistency) Reference object + temporal assume/guarantee Allows local specification of interface semantics Composable TileLink interface spec provides: Documentation of the interface Ability to reason formally about specification Efficient and rigorous test to find latent bugs Composable specifications provide a way to formal verification experts to provide value in an environment where most engineers do not have formal skills.

20 Specification as a social processThe specification develops over time in collaboration with the system architects. Ambiguities in informal specs must be resolved. Initial formal spec almost certainly does not reflect designers intention. Mismatch with implementation may indicate properties should be strengthened or weakened for efficiency. Over time the formal spec becomes a valuable document. Encapsulates design knowledge. Allows rigorous testing and verification.