proton6894

Automating Commutativity Analysis at the Design Level: 

Automating Commutativity Analysis at the Design Level Greg Dennis, Robert Seater, Derek Rayside, Daniel Jackson MIT CSAIL gdennis@mit.edu

Therac-25 (1985-1987): 

Therac-25 (1985-1987) race conditions when operator typed too quickly lacked hardware interlocks in previous versions X-rays delivered without metal target in place problems eluded testing 6 major overdoses, 2 deaths

Panama (2001): 

Panama (2001) déjà vu all over again unexpected data entry 20%-100% more radiation than prescribed 28 overdoses, at least 6 attributable deaths

Northeast Proton Therapy Center: 

Northeast Proton Therapy Center proton therapy machine at MGH unlike the Therac or Panama extensive hardware interlocks abundant runtime checks thoroughly reviewed and tested

NPTC Overview: 

NPTC Overview cyclotron

Automatic Beam Scheduler (ABS): 

room 2 room 3 Automatic Beam Scheduler (ABS) room 1 room 3 Request Queue allocated pending room 1

TCR Operations: 

TCR Operations RequestBeam RequestBeamHighPriority CancelBeamRequest ReleaseBeam Request(1) ReqHigh(3) Request(2) Cancel(1) Release(3)

MCR Operations: 

MCR Operations StepUp StepDown Flush FlushAll StepUp(1) Flush(3) StepDown(1) FlushAll()

Interfering Commands: 

Interfering Commands Request(1) Request(1) FlushAll() FlushAll() ≠

Commutativity: 

Commutativity if not, results can be surprising when commands issued simultaneously.

Violations of Commutativity: 

Violations of Commutativity Violation of Diamond Equivalence: Violation of Diamond Connectivity:

What We Did: 

What We Did Alloy Model OCL Spec of Beam Scheduler Commutativity Properties Commutativity Matrix Alloy Analyzer commutativity properties for each pair of operations

OCL Spec: 

OCL Spec context BeamScheduler::cancelBeamRequest(req: BeamRequest) pre: -- BeamRequest is inside the pending request queue self.pendingRequests@pre->exists(r | r == req) post: -- BeamRequest is not inside the pending requests queue not self.pendingRequests->exists(r | r == req) key differences between OCL and Alloy?

Slide14: 

open util/ordering[OrderID] sig Request { room: Room, priority: Priority } sig Room {} abstract sig Priority {} one sig Service, Normal, High extends Priority {} sig Queue { alloc, pending, requests : set Request, order: requests -> one OrderID }{ requests = alloc + pending } sig OrderID {}

Operations: 

Operations pred CancelBeamRequest(q, q': Queue, req: Request) { preCancelBeamRequest(q, req) q'.pending = q.pending - req q'.alloc = q.alloc q'.order = (q.requests – req) <: (q.order) } pred preCancelBeamRequest(q: Queue, req: Request) { req in q.pending } we factored out the precondition of each operation into a separate predicate effect of operation as constraint on pre- and post-state

Commutativity Properties: 

assert A_B_Equiv { all si, sa, sb, sab, sba: Queue { A(si,sa) && B(sa,sab) && B(si,sb) && A(sb,sba) => sab = sba } } assert Cancel_StepUp_Equiv { all si, sa, sb, sab, sba: Queue, rq1, rq2: Request { (Invariants(si) && CancelBeamRequest(si, sa, rq1) && StepUp(sa, sab, rq2) && StepUp(si, sb, rq2) && CancelBeamRequest(sb, sba, rq1)) => equivQueues(sab, sba) } } Commutativity Properties

Results: 

Results 3-100 seconds/analysis, Pentium III 600 MHz, 192 MB RAM TCR Operations TCR Operations MCR Operations

Non-commutativity Example: 

Non-commutativity Example ReqHigh(1) ReqHigh(1) Release(2) Release(2) cannot execute

Pure Logic Modeling: 

Pure Logic Modeling Could we have modeled commutativity in OCL with built-in state transitions? "Pure Logic Modeling": explicit states allows us to "rewind" time and ask about different execution traces Similar difficulty analyzing these properties with traditional model checker.

Conclusions: 

Conclusions Practical results from lightweight formal methods Commutativity analysis is useful when humans manipulate shared data Constraint solver effective for this analysis didn't stretch limits of tool or modelers Analyzability is important in practice Pure logic modeling is powerful