Skip to content
This repository has been archived by the owner on May 3, 2024. It is now read-only.

Commit

Permalink
fix typo
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Feb 8, 2024
1 parent 00d92c5 commit 8c57264
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 17 deletions.
12 changes: 6 additions & 6 deletions router/dataplane.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,12 +133,12 @@ type BatchConn interface {
// @ requires io.token(place) && MultiReadBio(place, prophecyM)
// @ preserves dp.Valid()
// @ ensures err == nil ==> prophecyM == n
// @ ensures err == nil ==> io.token(old(MutliReadBioNext(place, n))) && old(MutliReadBioCorrectIfs(place, n, ifsToIO_ifs(IngressID)))
// @ ensures err == nil ==> io.token(old(MultiReadBioNext(place, n))) && old(MultiReadBioCorrectIfs(place, n, ifsToIO_ifs(ingressID)))
// @ ensures err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> unfolding acc(msgs[i].Mem(), _) in absIO_val(dp, msgs[i].Buffers[0], IngressID) ==
// @ old(MutliReadBioIO_val(place, n)[i])
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> unfolding acc(msgs[i].Mem(), _) in absIO_val(dp, msgs[i].Buffers[0], ingressID) ==
// @ old(MultiReadBioIO_val(place, n)[i])
// TODO (Markus): uint16 or option[io.IO_ifs] for ingress
ReadBatch(msgs underlayconn.Messages /*@, ghost IngressID uint16, ghost prophecyM int, ghost place io.Place, ghost dp io.DataPlaneSpec @*/) (n int, err error)
ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place, ghost dp io.DataPlaneSpec @*/) (n int, err error)
// @ requires acc(addr.Mem(), _)
// @ requires acc(Mem(), _)
// @ preserves acc(sl.AbsSlice_Bytes(b, 0, len(b)), R10)
Expand Down Expand Up @@ -797,10 +797,10 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// @ ghost numberOfReceivedPacketsProphecy := AllocProphecy()
// @ ExtractMultiReadBio(dp, t, numberOfReceivedPacketsProphecy, s)
// @ MultiUpdateElemWitness(t, numberOfReceivedPacketsProphecy, ioIngressID, s, ioSharedArg)
// @ ghost ioValSeq := MutliReadBioIO_val(t,numberOfReceivedPacketsProphecy)
// @ ghost ioValSeq := MultiReadBioIO_val(t,numberOfReceivedPacketsProphecy)

// @ ghost sN := MultiReadBioUpd(t, numberOfReceivedPacketsProphecy, s)
// @ ghost tN := MutliReadBioNext(t, numberOfReceivedPacketsProphecy)
// @ ghost tN := MultiReadBioNext(t, numberOfReceivedPacketsProphecy)
// @ assert dp.dp3s_iospec_ordered(sN, tN)
pkts, err := rd.ReadBatch(msgs /*@, ingressID, numberOfReceivedPacketsProphecy, t , dp @*/)
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
Expand Down
22 changes: 11 additions & 11 deletions router/dataplane_concurrency_model.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,16 +74,16 @@ pred MultiReadBio(ghost t io.Place, ghost expectedPkts int) {
ghost
requires MultiReadBio(t, expectedPkts)
decreases expectedPkts
pure func MutliReadBioNext(ghost t io.Place, ghost expectedPkts int) (ghost tn io.Place) {
pure func MultiReadBioNext(ghost t io.Place, ghost expectedPkts int) (ghost tn io.Place) {
return expectedPkts <= 0 ? t : unfolding MultiReadBio(t, expectedPkts) in
MutliReadBioNext(io.dp3s_iospec_bio3s_recv_T(t), expectedPkts-1)
MultiReadBioNext(io.dp3s_iospec_bio3s_recv_T(t), expectedPkts-1)
}

// Checks that all packets are received from the same interface (key).
ghost
requires MultiReadBio(t, expectedPkts)
decreases expectedPkts
pure func MutliReadBioCorrectIfs(
pure func MultiReadBioCorrectIfs(
ghost t io.Place,
ghost expectedPkts int,
ghost k Key) bool {
Expand All @@ -95,18 +95,18 @@ pure func MutliReadBioCorrectIfs(
k == ifs
default:
false
} && MutliReadBioCorrectIfs(io.dp3s_iospec_bio3s_recv_T(t), expectedPkts-1, k)
} && MultiReadBioCorrectIfs(io.dp3s_iospec_bio3s_recv_T(t), expectedPkts-1, k)
}


ghost
requires 0 <= expectedPkts && MultiReadBio(t, expectedPkts)
ensures len(res) == expectedPkts
decreases expectedPkts
pure func MutliReadBioIO_val(ghost t io.Place, ghost expectedPkts int) (ghost res seq[io.IO_val]) {
pure func MultiReadBioIO_val(ghost t io.Place, ghost expectedPkts int) (ghost res seq[io.IO_val]) {
return expectedPkts <= 0 ? seq[io.IO_val]{} :
unfolding MultiReadBio(t, expectedPkts) in
seq[io.IO_val]{io.dp3s_iospec_bio3s_recv_R(t)} ++ MutliReadBioIO_val(
seq[io.IO_val]{io.dp3s_iospec_bio3s_recv_R(t)} ++ MultiReadBioIO_val(
io.dp3s_iospec_bio3s_recv_T(t), expectedPkts-1)
}

Expand Down Expand Up @@ -140,7 +140,7 @@ ghost
decreases n
requires dp.dp3s_iospec_ordered(s, t)
ensures MultiReadBio(t, n)
ensures dp.dp3s_iospec_ordered(MultiReadBioUpd(t, n, s), MutliReadBioNext(t, n))
ensures dp.dp3s_iospec_ordered(MultiReadBioUpd(t, n, s), MultiReadBioNext(t, n))
func ExtractMultiReadBio(
ghost dp io.DataPlaneSpec,
ghost t io.Place,
Expand All @@ -159,9 +159,9 @@ requires MultiReadBio(t, n)
requires ElemAuth(s.ibuf, y.IBufY) && ElemAuth(s.obuf, y.OBufY)
ensures MultiReadBio(t, n)
ensures MultiReadBioUpd(t, n, s) == old(MultiReadBioUpd(t, n, s))
ensures MutliReadBioNext(t, n) == old(MutliReadBioNext(t, n))
ensures MultiReadBioNext(t, n) == old(MultiReadBioNext(t, n))
ensures ElemAuth(MultiReadBioUpd(t, n, s).ibuf, y.IBufY) && ElemAuth(MultiReadBioUpd(t, n, s).obuf, y.OBufY)
ensures 0 <= n && MutliReadBioCorrectIfs(t, n, k) ==> MultiElemWitness(y.IBufY, k, MutliReadBioIO_val(t, n))
ensures 0 <= n && MultiReadBioCorrectIfs(t, n, k) ==> MultiElemWitness(y.IBufY, k, MultiReadBioIO_val(t, n))
decreases n
func MultiUpdateElemWitness(
ghost t io.Place,
Expand All @@ -180,8 +180,8 @@ func MultiUpdateElemWitness(
fold MultiReadBio(t, n)
}

if 0 <= n && MutliReadBioCorrectIfs(t, n, k) {
fold MultiElemWitness(y.IBufY, k, MutliReadBioIO_val(t, n))
if 0 <= n && MultiReadBioCorrectIfs(t, n, k) {
fold MultiElemWitness(y.IBufY, k, MultiReadBioIO_val(t, n))
}
}

Expand Down

0 comments on commit 8c57264

Please sign in to comment.