Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verify loops in Run #244

Merged
merged 11 commits into from
Feb 6, 2024
Merged

Verify loops in Run #244

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
40ab699
Run() loops
jcp19 Jan 30, 2024
6df6a7a
progress on the proof of closures
jcp19 Feb 2, 2024
18ea968
drop unnecessary import
jcp19 Feb 2, 2024
b5145a5
backup
jcp19 Feb 2, 2024
0d4b79e
backup
jcp19 Feb 2, 2024
9655d08
backup
jcp19 Feb 2, 2024
cd9569e
backup
jcp19 Feb 2, 2024
a3ca008
backup
jcp19 Feb 4, 2024
33b7b7c
backup
jcp19 Feb 4, 2024
ba12785
fix comment
jcp19 Feb 4, 2024
0431486
Update router/dataplane.go
jcp19 Feb 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion router/bfd/session_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
161 changes: 135 additions & 26 deletions router/dataplane.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
49 changes: 35 additions & 14 deletions router/dataplane_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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?
Expand Down Expand Up @@ -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)
}
Loading