/* ------------------------------------------------------------------------ MODEL OF LAYERS FOR STUDYING MOBILITY Copyright AT&T, 2011, 2012. This Alloy model is an appendix to the paper "Compositional Network Mobility" by Pamela Zave and Jennifer Rexford. This is a model of the shared, distributed state of each layer in a stack of layers. The model is simplified in two very important ways: 1) It contains only enough detail for a discussion of mobility. Many aspects and refinements are left out. There are also constraints that might not hold in the general case (these are noted). 2) It models a snapshot of the state, and is therefore completely static. This is sufficient for the purpose of defining and checking consistency conditions and dependencies. See below for information on what is verified, and how. ------------------------------------------------------------------------ */ /* ------------------------------------------------------------------------ BASIC TYPES ------------------------------------------------------------------------ */ sig Process { } sig Ident { } /* ------------------------------------------------------------------------ MACHINES AND LAYERS * As layers and their names are static, there is no distinction between a layer individual and its name. * Because a process only exists in this model as a member of a layer, and the name of a member process is unique and permanent for that member in that layer, there is no need to distinguish between a process individual and its name. ------------------------------------------------------------------------ */ sig Machine { supported: set Process } sig Layer { members: set Process, -- For layers serving overlays: overlays: set Layer, locations: set Registration, sessions: set Channel, -- For layers served by underlays: underlays: set Layer, attachments: set Registration, links: set Channel, -- For layers with routing: routes: set Route } /* ------------------------------------------------------------------------ RECORDS * A registration denotes a relation between two layers, and is part of the state of both layers. In the overlay, it is in the attachments, and the layer field indicates the underlay. In the underlay, it is in the locations, and the layer field indicates the overlay. * A channel also denotes a relation between two layers, and is also part of the state of both layers. In the overlay, it is in the links, and the layer field indicates the underlay. In the underlay, it is in the sessions, and the layer field indicates the overlay. * This definition of a route is based on a crude notion of routing and forwarding, without any concepts of paths. As such, it must be considered provisional, and is here for illustration only. ------------------------------------------------------------------------ */ sig Registration { layer: Layer, -- the other layer in the relationship attached: Process, -- the overlay process location: Process } -- the underlay process sig Channel { layer: lone Layer, -- the other layer in the relationship initiator: Process, -- both initiator and acceptor are acceptor: Process, -- overlay processes initIdent: Ident, -- both identifiers are unique for accptIdent: Ident } -- their process sig Route { from: Process, to: Process, route: Channel -- this is a link within the layer, on } -- which a message at "from" to "to" -- should be sent or forwarded /* ------------------------------------------------------------------------ CONSISTENCY CONDITIONS ON SETS ------------------------------------------------------------------------ */ fact ProcessBelongsToOneMachine { all p: Process | one supported.p } fact ProcessBelongsToOneLayer { all p: Process | one members.p } fact SelfNotInOverlays { all l: Layer | l ! in l.overlays } fact SelfNotInUnderlays { all l: Layer | l ! in l.underlays } fact OverlaysAndUnderlaysAgree { all o: Layer, u: Layer | o in u.overlays <=> u in o.underlays } fact LayerGraphIsAcyclic { all l: Layer | l ! in l.(^underlays) } assert LayerGraphHasTopAndBottom { some Layer => (some l: Layer | no l.overlays) && (some l: Layer | no l.underlays) } /* ------------------------------------------------------------------------ CONSISTENCY CONDITIONS ON REGISTRATIONS * A registration is created and destroyed at the initiative of either the attached or location process, in cooperation with the other process. * An overlay process can only be registered at one location in a particular underlay. This restriction is convenient for mobility. It is definitely too restrictive for multihoming, however. ------------------------------------------------------------------------ */ fact AttachmentsHaveConsistentLocalFields { all l: Layer, r: l.attachments | ( r.layer in l.underlays && r.attached in l.members ) } fact LocationsHaveConsistentLocalFields { all l: Layer, r: l.locations | ( r.layer in l.overlays && r.location in l.members ) } fact AttachedAndLocationOnSameMachine { all l: Layer, r: l.attachments | some m: Machine | r.attached + r.location in m.supported } fact EachAttachmentHasLocation { all o: Layer, ro: o.attachments | one ru: (ro.layer).locations | ro.attached = ru.attached && ro.location = ru.location } fact EachLocationHasAttachment { all u: Layer, ru: u.locations | one ro: (ru.layer).attachments | ro.attached = ru.attached && ro.location = ru.location } fact ProcessHasLoneLocationInLayer { all p: Process, l: Layer | lone r: l.locations | p = r.attached } assert ProcessHasLoneAttachmentInLayer { all p: Process, o, u: Layer | lone r: o.attachments | p = r.attached && u = r.layer } /* ------------------------------------------------------------------------ CONSISTENCY CONDITIONS ON CHANNELS * In this model the only communication service is a point-to-point, two- way message channel. This is really just an example, as many other services can be provided and/or used by layers. * The initiator and acceptor of a channel are its higher endpoints. Their locations are its lower endpoints. * A channel is usually created at the initiative of the initiator process, in cooperation with the acceptor process and both their location processes. One exception to this would be a static channel, created by layer initialization. Another exception to this might be signaling/ media separation, where other agents create a dynamic channel on behalf of its endpoints. * Destruction of a channel can be initiated by the initiator or acceptor. It can never be initiated by a location process. * If a layer has no underlays, then it implements its links internally. * In general, if a layer has no overlays, then it should be able to implement sessions for its own internal use. This is not included in this model, because it requires too much complication for too little value. In this model, a layer at the top of the hierarchy has no sessions. * Note that there is no global consistency between registrations and channels. A channel can exist without registrations (during movement), and a registration can exist without supporting a channel. ------------------------------------------------------------------------ */ fact LinksHaveConsistentLocalFields { all l: Layer, c: l.links | ( (c.layer in l.underlays || (no c.layer && no l.underlays) ) && (c.initiator + c.acceptor) in l.members && c.initiator != c.acceptor ) } fact SessionsHaveConsistentLocalFields { all l: Layer, c: l.sessions | c.layer in l.overlays } fact TopLayerHasNoSessions { all l: Layer | no l.overlays => no l.sessions } fact EndpointIdentifiersUniqueForTheirProcesses { all l: Layer, p: l.members, i: Ident | lone c: l.links | ( (p = c.initiator && i = c.initIdent ) || (p = c.acceptor && i = c.accptIdent) ) } fact InterlayerLinkHasSession { all o: Layer, co: o.links | some co.layer => ( one cu: (co.layer).sessions | co.initiator = cu.initiator && co.acceptor = cu.acceptor && co.initIdent = cu.initIdent && co.accptIdent = cu.accptIdent ) } fact SessionHasLink { all u: Layer, cu: u.sessions | one co: (cu.layer).links | co.initiator = cu.initiator && co.acceptor = cu.acceptor && co.initIdent = cu.initIdent && co.accptIdent = cu.accptIdent } /* ------------------------------------------------------------------------ CONSISTENCY CONDITIONS ON ROUTES * If a layer has no routes, then every process should be reachable from every other process. Either the layer implements complete connectivity internally, or every process is registered in the same underlay. ------------------------------------------------------------------------ */ fact RouteIsALink { all l: Layer, r: l.routes | r.route in l.links } fact RouteBeginsAtFromMember { all l: Layer, r: l.routes | r.from in (r.route.initiator + r.route.acceptor) } /* ------------------------------------------------------------------------ CONSISTENCY CHECKING NetworkExists is a predicate describing a realistic snapshot of the layer stack with 4 layers on 3 levels. A link at the highest level is implemented by a session at the middle level. The session traverses 2 links at the middle level, each of which is implemented by a session in a different layer at the bottom level. The Alloy Analyzer shows that this predicate can be instantiated, which means that the model is mathematically consistent. ------------------------------------------------------------------------ */ pred NetworkExists { some disj ml, mm, mr: Machine, disj la, li, ll, lw: Layer, disj p0, p1, p2, p3, p4, p5, p6, p7, p8: Process, disj r0, r1, r2, r3l, r3r, r4: Registration, disj l0, l1, l2: Channel, disj u23, u24, u32, u34, u42, u43: Route | (p0+p2+p5) in ml.supported && (p3+p6+p7) in mm.supported && (p1+p4+p8) in mr.supported && li = la.underlays && la = li.overlays && (ll + lw) = li.underlays && no ll.underlays && no lw.underlays && (p0+p1) in la.members && (p2+p3+p4) in li.members && (p5+p6) in ll.members && (p7+p8) in lw.members && (r0+r1) in la.attachments && (r2+r3l+r3r+r4) in li.attachments && r0.attached = p0 && r0.location = p2 && r1.attached = p1 && r1.location = p4 && r2.attached = p2 && r2.location = p5 && r3l.attached = p3 && r3l.location = p6 && r3r.attached = p3 && r3r.location = p7 && r4.attached = p4 && r4.location = p8 && l0 in la.links && l0.initiator = p0 && l0.acceptor = p1 && (l1+l2) in li.links && l1.initiator = p2 && l1.acceptor = p3 && l2.initiator = p3 && l2.acceptor = p4 && l2.layer = lw && (u23 + u24 + u32 + u34 + u42 + u43) in li.routes && u23.from = p2 && u23.to = p3 && u23.route = l1 && u24.from = p2 && u24.to = p4 && u24.route = l1 && u32.from = p3 && u32.to = p2 && u32.route = l1 && u34.from = p3 && u34.to = p4 && u34.route = l2 && u42.from = p4 && u42.to = p2 && u42.route = l2 && u43.from = p4 && u43.to = p2 && u43.route = l2 } run NetworkExists for 1 but 3 Machine, 4 Layer, 9 Process, 12 Registration, 6 Channel, 2 Ident, 6 Route /* ------------------------------------------------------------------------ ASSERTIONS Checking has determined that these assertions are valid. ------------------------------------------------------------------------ */ check ProcessHasLoneAttachmentInLayer for 8 check LayerGraphHasTopAndBottom for 6 /* ------------------------------------------------------------------------ DEPENDENCIES Assume that machines and layers are static, as are the overlay/underlay relation. So dependencies on them are not an issue. Within a layer, because of AttachmentsHaveConsistentLocalFields, attachments depend on members; because of LocationsHaveConsistentLocalFields, locations depend on members; because of LinksHaveConsistentLocalFields, links depend on members; because of RouteIsALink, routes depend on links. ------------------------------------------------------------------------ */