Verify loops in Run (#244)

* Run() loops * progress on the proof of closures * drop unnecessary import * backup * backup * backup * backup * backup * backup * fix comment * Update router/dataplane.go
viperproject · Feb 6, 2024 · 685c562 · 685c562
1 parent 32c592e
commit 685c562
Show file tree

Hide file tree

Showing 3 changed files with 177 additions and 41 deletions.
diff --git a/router/bfd/session_spec.gobra b/router/bfd/session_spec.gobra
@@ -27,4 +27,10 @@ import (
 	"github.com/scionproto/scion/pkg/private/serrors"
 )
 
-var AlreadyRunning = serrors.New("is running")
+var AlreadyRunning = serrors.New("is running")
+
+ghost
+ensures AlreadyRunning != nil && AlreadyRunning.ErrorMem()
+ensures isComparable(AlreadyRunning)
+decreases
+func EstablishAlreadyRunning()
diff --git a/router/dataplane.go b/router/dataplane.go
@@ -680,16 +680,20 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro
 // after calling this method.
 // @ requires  acc(&d.running, 1/2) && !d.running
 // @ requires  acc(&d.Metrics, 1/2) && d.Metrics != nil
+// @ requires  acc(&d.svc, 1/2) && d.svc != nil
+// @ requires  acc(&d.internal, 1/2) && d.internal != nil
 // @ requires  acc(&d.macFactory, 1/2) && d.macFactory != nil
 // @ requires  acc(&d.forwardingMetrics, 1/2) && acc(d.forwardingMetrics, 1/2)
-// @ requires  0 in domain(d.forwardingMetrics)
 // @ requires  d.mtx.LockP()
 // @ requires  d.mtx.LockInv() == MutexInvariant!<d!>;
-// TODO: put well configured here
+// @ requires  acc(ctx.Mem(), _)
+// @ requires  acc(&d.mtx, _)
 func (d *DataPlane) Run(ctx context.Context) error {
 	// @ share d, ctx
 	d.mtx.Lock()
 	// @ unfold MutexInvariant!<d!>()
+	// @ assert d.forwardingMetrics != nil
+	// @ assert acc(&d.forwardingMetrics, _) && acc(d.forwardingMetrics, _)
 	d.running = true
 
 	d.initMetrics()
@@ -955,33 +959,136 @@ func (d *DataPlane) Run(ctx context.Context) error {
 			}
 		}
 
-	// (VerifiedSCION) Continue from here after adapting processPkt and processOHP
-	// @ TODO()
-	for k, v := range d.bfdSessions {
-		// @ TODO()
-		go func(ifID uint16, c bfdSession) {
-			// @ TODO()
-			defer log.HandlePanic()
-			if err := c.Run(ctx); err != nil && err != bfd.AlreadyRunning {
-				log.Error("BFD session failed to start", "ifID", ifID, "err", err)
+	// @ fold acc(MutexInvariant(d), R55)
+	// @ assert 0 in d.getDomForwardingMetrics()
+	// (VerifiedSCION) the following cannot be expressed as a pre-condition:
+	// there is really no way of specifying that the dataplane protected by the lock
+	// satisfies this condition.
+	// @ assume d.WellConfigured()
+
+	// @ ghost if d.bfdSessions != nil { unfold acc(accBfdSession(d.bfdSessions), R2) }
+
+	// (VerifiedSCION) we introduce this to avoid problems with the invariants that
+	// are generated by Gobra. In particular, the iterator bounds need access to
+	// d.bfdSessions, but because it is shared, we need to pass permission to it
+	// in the invariant. Unfortunately, the invariants that are passed by the user are
+	// put after those that are generated. Introducing this auxioliary variable sidesteps
+	// the issue with the encoding.
+	bfds := d.bfdSessions
+
+	// @ invariant bfds != nil ==> acc(bfds, R4)
+	// @ invariant bfds != nil ==> acc(accBfdSession(bfds), R4)
+	// @ invariant acc(&ctx, _) && acc(ctx.Mem(), _)
+	// @ decreases len(bfds) - len(visited)
+	for k, v := range bfds /*@ with visited @*/ {
+		cl :=
+			// @ requires c != nil && acc(c.Mem(), _)
+			// @ requires acc(&ctx, _) && acc(ctx.Mem(), _)
+			func /*@ closure1 @*/ (ifID uint16, c bfdSession) {
+				defer log.HandlePanic()
+				// @ bfd.EstablishAlreadyRunning()
+				if err := c.Run(ctx); err != nil && err != bfd.AlreadyRunning {
+					log.Error("BFD session failed to start", "ifID", ifID, "err", err)
+				}
 			}
-		}(k, v) // @ as closureSpec1
+		// @ getBfdSessionMem(v, bfds)
+		go cl(k, v) // @ as closure1
+	}
+
+	// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), R2) }
+
+	// (VerifiedSCION) we introduce this to avoid problems with the invariants that
+	// are generated by Gobra. In particular, the iterator bounds need access to
+	// d.bfdSessions, but because it is shared, we need to pass permission to it
+	// in the invariant. Unfortunately, the invariants that are passed by the user are
+	// put after those that are generated. Introducing this auxioliary variable sidesteps
+	// the issue with the encoding.
+	externals := d.external
+
+	// @ invariant acc(&read, _) && read implements rc
+	// @ invariant acc(&d, _)
+	// @ invariant acc(&d.external, _) && d.external === externals
+	// @ invariant acc(MutexInvariant(d), _) && d.WellConfigured()
+	// @ invariant externals != nil ==> acc(externals, R4)
+	// @ invariant externals != nil ==> acc(accBatchConn(externals), R4)
+	// @ invariant acc(&d, _)
+	// @ invariant acc(d,  _)
+	// @ invariant acc(MutexInvariant(d), _) && d.WellConfigured()
+	// @ invariant d.getValSvc() != nil
+	// @ invariant d.getValForwardingMetrics() != nil
+	// @ invariant 0 in d.getDomForwardingMetrics()
+	// @ invariant d.macFactory != nil
+	// @ decreases len(externals) - len(visited)
+	for ifID, v := range externals /*@ with visited @*/ {
+		cl :=
+			// @ requires acc(&read, _) && read implements rc
+			// @ requires acc(&d, _)
+			// @ requires acc(d,  _)
+			// @ requires acc(MutexInvariant(d), _) && d.WellConfigured()
+			// @ requires d.getValSvc() != nil
+			// @ requires d.getValForwardingMetrics() != nil
+			// @ requires 0 in d.getDomForwardingMetrics()
+			// @ requires i in d.getDomForwardingMetrics()
+			// @ requires d.macFactory != nil
+			// @ requires c != nil && acc(c.Mem(), _)
+			func /*@ closure2 @*/ (i uint16, c BatchConn) {
+				defer log.HandlePanic()
+				// @ assert read implements rc
+				// (VerifiedSCION) check preconditions of call to read(i, c) manually.
+				// @ assert acc(&d, _)
+				// @ assert acc(d,  _)
+				// @ assert acc(MutexInvariant(d), _) && d.WellConfigured()
+				// @ assert d.getValSvc() != nil
+				// @ assert d.getValForwardingMetrics() != nil
+				// @ assert 0 in d.getDomForwardingMetrics()
+				// @ assert i in d.getDomForwardingMetrics()
+				// @ assert d.macFactory != nil
+				// @ assert c != nil && acc(c.Mem(), _)
+
+				// (VerifiedSCION) Skip automated verification of the call due to a
+				// bug in Gobra. (https://github.com/viperproject/gobra/issues/723)
+				// @ TODO()
+				read(i, c) //@ as rc
+			}
+		// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), R50) }
+		// @ assert v in range(d.external)
+		// @ assert acc(v.Mem(), _)
+		// @ d.InDomainExternalInForwardingMetrics3(ifID)
+		// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), R50) }
+		go cl(ifID, v) //@ as closure2
 	}
-	for ifID, v := range d.external {
-		go func(i uint16, c BatchConn) {
-			// @ TODO()
+	cl :=
+		// @ requires acc(&read, _) && read implements rc
+		// @ requires acc(&d, _)
+		// @ requires acc(d,  _)
+		// @ requires acc(MutexInvariant(d), _) && d.WellConfigured()
+		// @ requires d.getValSvc() != nil
+		// @ requires d.getValForwardingMetrics() != nil
+		// @ requires 0 in d.getDomForwardingMetrics()
+		// @ requires d.macFactory != nil
+		// @ requires c != nil && acc(c.Mem(), _)
+		func /*@ closure3 @*/ (c BatchConn) {
 			defer log.HandlePanic()
-			// TODO(VerifiedSCION): calling this may cause problems because of the lack of permissions to d.mtx
-			// This should be easily addressable nonethelss
-			read(i, c) //@ as readClosureSpec // TODO: maybe use rc as the spec instead and delete readClosureSpec
-		}(ifID, v) //@ as closureSpec2
-	}
-	go func(c BatchConn) {
-		// @ TODO()
-		defer log.HandlePanic()
-		// TODO(VerifiedSCION): calling this may cause problems because of the lack of permissions to d.mtx
-		read(0, c) //@ as readClosureSpec  // TODO: maybe use rc as the spec instead and delete readClosureSpec
-	}(d.internal) //@ as closureSpec3
+			// @ assert read implements rc
+
+			// (VerifiedSCION) once again, check preconditions of call to read(0, c)
+			// manually, due to a completness issue with closures:
+			// https://github.com/viperproject/gobra/issues/723.
+			// @ assert acc(&d, _)
+			// @ assert acc(d,  _)
+			// @ assert acc(MutexInvariant(d), _) && d.WellConfigured()
+			// @ assert d.getValSvc() != nil
+			// @ assert d.getValForwardingMetrics() != nil
+			// @ assert 0 in d.getDomForwardingMetrics()
+			// @ assert d.macFactory != nil
+			// @ assert c != nil && acc(c.Mem(), _)
+
+			// (VerifiedSCION) Skip automated verification and rely on manual
+			// checks above.
+			// @ TODO()
+			read(0, c) //@ as rc
+		}
+	go cl(d.internal) //@ as closure3
 
 	// (VerifiedSCION) we ignore verification from this point onward because of the
 	// call to Unlock. Supporting it is conceptually easy, but it requires changing
@@ -1010,6 +1117,7 @@ func (d *DataPlane) Run(ctx context.Context) error {
 // @ preserves acc(&d.internalNextHops, R15)
 // @ preserves d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), R15)
 // @ ensures   accForwardingMetrics(d.forwardingMetrics)
+// @ ensures   0 in d.DomainForwardingMetrics()
 // @ decreases
 func (d *DataPlane) initMetrics() {
 	// @ preserves acc(&d.forwardingMetrics)
@@ -1037,6 +1145,7 @@ func (d *DataPlane) initMetrics() {
 	// @ invariant d.external != nil ==> acc(d.external, R20)
 	// @ invariant d.external === old(d.external)
 	// @ invariant acc(&d.forwardingMetrics) && acc(d.forwardingMetrics)
+	// @ invariant 0 in domain(d.forwardingMetrics)
 	// @ invariant acc(&d.internalNextHops, R15)
 	// @ invariant d.internalNextHops === old(d.internalNextHops)
 	// @ invariant d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), R15)

diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra
@@ -77,7 +77,7 @@ pred accAddr(addrs map[uint16]*net.UDPAddr) {
 pred accBatchConn(batchConns map[uint16]BatchConn) {
 	acc(batchConns, 1/2) &&
 	forall b BatchConn :: { b in range(batchConns) }{ b.Mem() } b in range(batchConns) ==>
-		b.Mem()
+		b!= nil && acc(b.Mem(), _)
 }
 
 pred accBfdSession(bfdSessions map[uint16]bfdSession) {
@@ -426,19 +426,18 @@ func (d *DataPlane) getNewPacketProcessorFootprint() {
 
 /**** End of acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/
 
-/** Start of closure specs for the Run method **/
-requires true
-func readClosureSpec(ingressID uint16, rd BatchConn)
-
-requires true
-func closureSpec1(ifID uint16, c bfdSession)
-
-requires true
-func closureSpec2(i uint16, c BatchConn)
-
-requires true
-func closureSpec3(c BatchConn)
-/** End of closure specs for the Run method **/
+ghost
+requires bfdSessions != nil ==> acc(bfdSessions, R50)
+requires v in range(bfdSessions)
+requires acc(accBfdSession(bfdSessions), R50)
+ensures  bfdSessions != nil ==> acc(bfdSessions, R50)
+ensures  acc(accBfdSession(bfdSessions), R50)
+ensures  v != nil && acc(v.Mem(), _)
+decreases
+func getBfdSessionMem(v bfdSession, bfdSessions map[uint16]bfdSession) {
+	unfold acc(accBfdSession(bfdSessions), R55)
+	fold acc(accBfdSession(bfdSessions), R55)
+}
 
 /** definitions used internally for the proof of Run **/
 // TODO: maybe drop and use the invariant of Messages instead now that we have IsActive?
@@ -623,4 +622,26 @@ decreases
 func (d *DataPlane) InDomainExternalInForwardingMetrics2(id uint16) {
 	unfold acc(MutexInvariant(d), _)
 	unfold acc(accBatchConn(d.external), _)
+}
+
+// This lemma has the same exact spec as before, except for a fixed permission to d.
+// external. Although simple, this requires some work to prove to avoid incompletnesses
+// with MCE.
+ghost
+requires acc(MutexInvariant(d), _) && d.WellConfigured()
+requires acc(&d.external, _) && acc(d.external, R55)
+requires id in domain(d.external)
+ensures  acc(MutexInvariant(d), _)
+ensures  acc(&d.external, _) && acc(d.external, R55)
+ensures  id in d.getDomForwardingMetrics()
+decreases
+func (d *DataPlane) InDomainExternalInForwardingMetrics3(id uint16)
+
+ghost
+requires acc(&d.forwardingMetrics, _)
+requires acc(accForwardingMetrics(d.forwardingMetrics), _)
+decreases
+pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] {
+	return unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in
+		domain(d.forwardingMetrics)
 }