| \documentclass[a4paper,9pt,twoside]{article} |
| \usepackage{zed-cm} |
| \usepackage{graphicx} |
| %\markboth{Draft}{Draft} |
| \pagestyle{myheadings} |
| \begin{document} |
| \parskip 6 pt |
| \parindent 0 pt |
| |
| \title{Regions in Virgo (v0.9)} |
| \author{Glyn Normington\\Steve Powell} |
| |
| \maketitle |
| \thispagestyle{myheadings} |
| \pagenumbering{alph} |
| \setcounter{page}{0} |
| |
| %============================================================================= |
| This document provides a formal model of how Virgo divides the OSGi framework into a directed graph |
| of \textit{regions}. |
| |
| The model informed the work on \textbf{Bug 330776} ``Re-implement user region using |
| framework hooks instead of nested framework''. |
| |
| The model is defined using the Z specification language. An introduction provides an informal |
| description of regions and how they influence framework hooks for readers who are not familiar with Z. |
| |
| We are grateful to Rob Harrop for reviewing this model and raising several corrections and |
| points of clarification and to Dave Kemper for pointing out an inconsistency. |
| |
| \clearpage |
| \pagenumbering{roman} |
| \tableofcontents |
| |
| % Type checking hacks |
| \newcommand{\true}{true} |
| \newcommand{\false}{false} |
| \renewcommand{\emptyset}{\varnothing} |
| \newcommand{\ModuleDefZero}{ModuleDef_0} |
| \newcommand{\ModuleDefOne}{ModuleDef_1} |
| \newcommand{\ModuleDefTwo}{ModuleDef_2} |
| \newcommand{\ModuleDefThree}{ModuleDef_3} |
| \newcommand{\ModuleDefFour}{ModuleDef_4} |
| |
| %============================================================================= |
| \clearpage |
| \pagenumbering{arabic} |
| \section{Introduction} |
| \label{cha:intro} |
| |
| The Virgo kernel is isolated from applications by the use of \textit{regions}. |
| The kernel runs in its own region and applications run in a \textit{user region}. |
| |
| Virgo 2.1.0 implemented the user region as a nested framework, but Equinox |
| has deprecated the nested framework support in favour of \textit{framework hooks} |
| which are being defined for OSGi R4.3. |
| \textbf{Bug 330776} re-implements the user region using the OSGi framework and service |
| registry hooks. |
| |
| Framework hooks are used to limit which bundles can `see' particular bundles |
| and exported packages, and service registry hooks are used to limit which bundles |
| can `see' particular services. `Seeing' includes both finding and being notified via lifecycle events. |
| |
| Rather than allowing arbitrary hook behaviour, we limit the hooks to operate on regions |
| which are connected together with filters. |
| |
| A \textit{region} is then a set of bundles and a region can see bundles, exported packages, and services |
| from another region via a \textit{connection}. Each connection has a \textit{filter} which may limit |
| what can be seen across the connection. |
| Hence regions and connections form a directed graph decorated by filters. |
| |
| For example, Figure \ref{fig:conn} shows three regions connected by three connections. |
| Each connection has a filter which limits what bundles, exported packages, and services |
| are visible across the connection. |
| |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.35]{connected-regions.pdf} |
| \caption{Connected Regions} |
| \end{center} |
| \label{fig:conn} |
| \end{figure} |
| |
| A connection may be thought of as an import. So region C imports from region B. |
| The imports are filtered, so filter h may limit what region C sees from region B. |
| Similarly region A imports from region B through filter f and region B imports from region A through |
| filter g. |
| |
| Unlike OSGi package imports between bundles, imports between regions are transitive. |
| So region C can see bundles, exported packages, and services from region A, subject to filters g and h. |
| |
| We now consider visibility from the perspective of each of the framework hooks. |
| |
| \subsection{Bundle Find Hook} |
| |
| The bundle find hook limits the bundles that a bundle in a given region sees when listing bundles using |
| \texttt{BundleContext.getBundles}. |
| |
| For example, Figure \ref{fig:bfind} shows a bundle W which finds bundles W, X, and Y. |
| It does not find Z which is filtered out. |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.4]{bundle-find.pdf} |
| \caption{Bundle Find \label{fig:bfind}} |
| \end{center} |
| \end{figure} |
| |
| \subsection{Bundle Event Hook} |
| |
| The bundle event hook limits the bundle events that a bundle listener in a given region receives. |
| |
| For example, Figure \ref{fig:bevent} shows a bundle W which has a bundle listener. |
| Bundle W's bundle listener receives events for W, X, and Y. It does not receive events for bundle Z which is filtered out. |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.4]{bundle-event.pdf} |
| \caption{Bundle Event \label{fig:bevent}} |
| \end{center} |
| \end{figure} |
| |
| \subsection{Service Find Hook} |
| |
| The service find hook limits the services that a bundle in a given region sees when looking up services. |
| |
| For example, Figure \ref{fig:sfind} shows a bundle W which can look up services s and t but not u which is filtered out. |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.4]{service-find.pdf} |
| \caption{Service Find \label{fig:sfind}} |
| \end{center} |
| \end{figure} |
| |
| \subsection{Service Event Hook} |
| |
| The service event hook limits the service events that a service listener in a given region receives. |
| |
| For example, Figure \ref{fig:sevent} shows a bundle W which has a service listener. |
| Bundle W's service listener receives events for s and t. It does not receive events for service u which is filtered out. |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.4]{service-event.pdf} |
| \caption{Service Event \label{fig:sevent}} |
| \end{center} |
| \end{figure} |
| |
| \subsection{Resolver Hook} |
| |
| The resolver hook limits the exported packages that the bundles in a given region may wire to, depending on |
| the region containing the bundle that exports each candidate exported package and the filters between the |
| regions. |
| |
| For example, Figure \ref{fig:pfilt} shows a bundle Z being resolved which imports packages p and q. Bundle X |
| in region B exports both p and q while bundle Y in region B exports only p. |
| |
| Region A is connected to region B with a filter that allows only package p to be seen by region A. |
| The net effect is that the import of p may be satisfied by either bundle X or Y but the import of package q may not |
| be satisfied by bundle X since q is filtered out. |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.4]{package-filtering.pdf} |
| \caption{Package Filtering \label{fig:pfilt}} |
| \end{center} |
| \end{figure} |
| |
| Another example in Figure \ref{fig:tpfilt} shows a package p transitively visible through two filters via an |
| intermediate region. |
| |
| Bundle Z may wire to bundle X or bundle Y for package p, but not for packages q and r which are both |
| filtered out on the way from C to A. |
| \begin{figure}[h!] |
| \begin{center} |
| \includegraphics*[scale=0.4]{transitive-package-filtering.pdf} |
| \caption{Transitive Package Filtering \label{fig:tpfilt}} |
| \end{center} |
| \end{figure} |
| |
| The remaining chapters provide a formal, albeit partial, model of bundles, regions, filters, and how |
| regions are connected together, via filters, into a directed graph. |
| The model finally defines the behaviour of framework hooks in terms of the directed graph of regions. |
| |
| %============================================================================= |
| \clearpage |
| \section{Basic Types} |
| \label{cha:basics} |
| |
| Some basic types define the primitives used in the model. |
| |
| \subsection*{Bundles} |
| |
| Bundles are uniquely identified in the OSGi framework by a bundle location, whose details are not |
| important here. |
| \begin{zed} |
| [BLoc] |
| \end{zed} |
| Note that, as of OSGi R4.3, when the framework property \texttt{org.osgi.framework.bsnversion} |
| is set to \texttt{multiple}, the combination of bundle symbolic name and bundle version is no |
| longer guaranteed to uniquely identify a bundle in the OSGi framework. |
| |
| \subsection*{Packages} |
| |
| We do not need the notion of package version and the attributes associated with package imports |
| and exports, so we simply declare a set of package objects. |
| \begin{zed} |
| [Package] |
| \end{zed} |
| |
| \subsection*{Services} |
| |
| Neither do we need details of services. |
| \begin{zed} |
| [Service] |
| \end{zed} |
| |
| %============================================================================= |
| \clearpage |
| \section{Bundle} |
| \label{cha:bundle} |
| |
| A bundle has a location, exports zero or more packages, and publishes zero or more services. |
| \begin{schema}{Bundle} |
| location : BLoc \\ |
| exportedPackages : \power Package \\ |
| publishedServices : \power Service \\ |
| \end{schema} |
| It is unusual, and usually bad practice, to include the primary key (in this case the $location$) of |
| an entity in the entity's schema. |
| We do it here to ensure that all bundles are |
| distinct and use this property later when determining which region a bundle belongs to. |
| |
| %============================================================================= |
| \clearpage |
| \section{Region} |
| \label{cha:region} |
| |
| We build up to a definition of a region in several small steps. |
| |
| \subsection{Proto-Region} |
| |
| A proto-region is a set of bundles. |
| These are intended to represent the bundles installed in the framework and associated with the proto-region. |
| \begin{schema}{ProtoRegion} |
| localBundles : \power Bundle \\ |
| \end{schema} |
| |
| \subsection{Indexed Region} |
| |
| An indexed region is a proto-region with an index of a certain sort. |
| |
| The index is a function identifying the bundles in the region by location. |
| \begin{schema}{IndexedRegion} |
| ProtoRegion \\ |
| l : BLoc \pinj Bundle \\ |
| \where |
| l = \{ b : localBundles @ b.location \mapsto b \} \\ |
| \end{schema} |
| The signature imposes the constraint of injectivity on the index. |
| Thus an indexed region is a set of bundles each of which is uniquely identified |
| by its location. |
| Notice that \textbf{all} the bundles in the proto-region are indexed. |
| |
| \subsection{OpenRegion} |
| |
| An open region is an indexed region with some derived sets of packages exported by bundles in the region |
| and services published by bundles in the region. |
| |
| \begin{schema}{OpenRegion} |
| IndexedRegion \\ |
| localPkg : \power Package \\ |
| localSvc : \power Service \\ |
| \where |
| localPkg = \bigcup \{ b : localBundles @ b.exportedPackages \} \\ |
| localSvc = \bigcup \{ b : localBundles @ b.publishedServices \} \\ |
| \end{schema} |
| %We allow a given exported package to be associated with more than one bundle, |
| %which can happen if a bundle uses |
| %\texttt{require-bundle} with the reexport option. |
| %We also allow a given service to be published by more than one bundle, |
| %which can never happen, but which causes |
| %no difficulty for this model and would complicate the model if we constrained it. |
| |
| \subsection{LinkedRegion} |
| |
| A linked region is an open region with additional sets of imported bundles, packages, and services. |
| |
| \begin{schema}{LinkedRegion} |
| OpenRegion \\ |
| importedBundles : \power Bundle \\ |
| importedPkg : \power Package \\ |
| importedSvc : \power Service \\ |
| \end{schema} |
| The imported bundles, packages, and services come into play later when regions are filtered and combined |
| because it will be possible to filter out a bundle but not its exported packages or published services. |
| We want to represent the result as a region for simplicity, so the region needs to have a way |
| of recording packages and services which are `detached' from their bundle(s). |
| |
| \subsection{Region} |
| |
| A region is a linked region in which we derive sets of all bundles, all packages, and all services. |
| \begin{schema}{Region} |
| LinkedRegion \\ |
| bundles : \power Bundle \\ |
| pkg : \power Package \\ |
| svc : \power Service \\ |
| \where |
| bundles = localBundles \cup importedBundles \\ |
| pkg = localPkg \cup importedPkg \\ |
| svc = localSvc \cup importedSvc \\ |
| \end{schema} |
| The local and imported packages are not necessarily disjoint and neither are the local and imported |
| services. This is important as packages exported by and services published by imported bundles |
| are classified as both local and imported. |
| |
| We define a nil region with no local or imported bundles, packages, or services. |
| \begin{axdef} |
| NIL : Region \\ |
| \where |
| NIL.bundles = \emptyset \\ |
| NIL.pkg = \emptyset \\ |
| NIL.svc = \emptyset \\ |
| \end{axdef} |
| |
| \subsection{Adding a Bundle to a Region} |
| |
| Bundles are typically added to regions \textit{as part of} the bundle install operation |
| so that the bundle is associated with its region by the time the |
| install completes. |
| |
| A bundle may also be added to a region after the bundle is installed, although this opens up a window in |
| which the bundle does not belong to any region. |
| |
| A bundle can be added to a region provided the region does not already contain a bundle with |
| the given bundle's location. |
| \begin{schema}{RegionAddBundleOk} |
| \Delta Region \\ |
| b? : Bundle \\ |
| \where |
| b?.location \notin \dom l \\ |
| bundles' = bundles \cup \{ b? \} \\ |
| importedPkg' = importedPkg \\ |
| importedSvc' = importedSvc \\ |
| \end{schema} |
| Note that $l'$, $localPkg'$, $localSvc'$, $pkg'$, and $svc'$ are determined by the constraints of $Region'$. |
| |
| \subsection{Combining Regions} |
| |
| Although we will not support operations to combine regions, it is necessary to define how to combine |
| regions so we can discuss the behaviour of directed graphs of regions later. |
| |
| %%inop \sqcup 3 |
| Regions with consistent indexing may be combined to produce a composite region using the infix $\sqcup$ operator. |
| \begin{axdef} |
| \_ \sqcup \_ : Region \cross Region \pfun Region \\ |
| \where |
| (\_ \sqcup \_) = (\lambda r1, r2 : Region @ \\ |
| \t3 (\mu Region | \\ |
| \t4 bundles = r1.bundles \cup r2.bundles \land \\ |
| \t4 pkg = r1.pkg \cup r2.pkg \land \\ |
| \t4 svc = r1.svc \cup r2.svc)) \\ |
| \end{axdef} |
| The precondition of $\sqcup$ is that no bundle in one region has the same location as a bundle in the other region. |
| |
| $\sqcup$ is idempotent, commutative, and associative (where defined) and $NIL$ acts as a zero. |
| \begin{argue} |
| \shows \forall r, s,t : Region | \{ (r, s), (s, t), (t, r) \} \subseteq \dom(\_ \sqcup \_) @ \\ |
| \t1 (r, r) \in \dom(\_ \sqcup \_) \land r \sqcup r = r \land \\ |
| \t1 (s, r) \in \dom(\_ \sqcup \_) \land r \sqcup s = s \sqcup r \land \\ |
| \t1 (r, s \sqcup t) \in \dom(\_ \sqcup \_) \land (r \sqcup s, t) \in \dom(\_ \sqcup \_) \land r \sqcup (s \sqcup t) = (r \sqcup s) \sqcup t \land \\ |
| \t1 (r, NIL) \in \dom(\_ \sqcup \_) \land r \sqcup NIL = NIL \\ |
| \end{argue} |
| |
| We define the set of all pairwise consistent regions |
| \begin{zed} |
| ConsistentRegionPairs == \dom(\_ \sqcup \_) \\ |
| \end{zed} |
| and the set of all pairwise consistent finite sets of regions. |
| \begin{zed} |
| ConsistentRegionSets == \{ f : \finset Region | \forall r, s : f @ (r, s) \in ConsistentRegionPairs \} \\ |
| \end{zed} |
| |
| Since $\sqcup$ is commutative, associative, idempotent, and has a zero, we define a distributed form. |
| \begin{axdef} |
| \bigsqcup : \finset Region \pfun Region \\ |
| \where |
| \bigsqcup \emptyset = NIL \land \\ |
| (\forall r : Region; f : \finset Region | \{ r \} \cup f \in ConsistentRegionSets @ \\ |
| \t1 \bigsqcup( \{ r \} \cup f ) = r \sqcup \bigsqcup f) \\ |
| \end{axdef} |
| |
| %============================================================================= |
| \clearpage |
| \section{Multiple Regions} |
| \label{cha:multiregions} |
| |
| We now describe a system comprising multiple regions. |
| |
| Regions are identified by a region identifier, whose details are not important here. |
| \begin{zed} |
| [RId] |
| \end{zed} |
| |
| The system of multiple regions has a collection of regions indexed by region identifier. |
| The collection is finite so that certain operations, described later, are well defined. |
| |
| The system has convenience sets of all the bundles and of all the region identifiers in the system. |
| These sets are derived from the indexed collection. |
| |
| The system also has a function for determining the region identifier of any bundle in the system from the |
| bundle's location. |
| \begin{schema}{Regions} |
| reg : RId \ffun Region \\ |
| allBundles : \power Bundle \\ |
| rids : \power RId \\ |
| breg : BLoc \pfun RId \\ |
| \where |
| allBundles = \bigcup \{ r : \ran reg@ r.bundles \} \\ |
| rids = \dom reg \\ |
| breg = \{ b : Bundle; rid : rids | b \in (reg~rid).bundles @ (b.location, rid) \} \\ |
| \end{schema} |
| Since $breg$ is a function, no bundle location can belong to more than one region. |
| Since a bundle's location uniquely identifies the bundle in its region, it follows that a bundle's location uniquely identifies the bundle in the system of multiple regions. |
| |
| \subsection{Determining a Bundle's Region} |
| |
| We expose the convenience function as an operation for determining a bundle's region. |
| \begin{schema}{GetRegionOk} |
| \Xi Regions \\ |
| b? : Bundle \\ |
| r! : Region \\ |
| \where |
| b? \in allBundles \\ |
| r! = reg(breg~b?.location) \\ |
| \end{schema} |
| |
| \subsection{Promoting Region Operations} |
| |
| We define a fairly standard schema for promoting operations on a single region into |
| operations on the system of multiple regions. |
| The region to be operated on is singled out using a region identifier and all other regions are left |
| unchanged. |
| \begin{schema}{PromoteRegion} |
| \Delta Regions \\ |
| \Delta Region \\ |
| rid? : RId \\ |
| \where |
| rid? \in \dom reg \\ |
| \theta Region = reg~rid? \\ |
| reg' = reg \oplus \{ rid? \mapsto \theta Region' \} \\ |
| \end{schema} |
| |
| Then we promote the operation to add a bundle. |
| \begin{zed} |
| RegionsAddBundleOk \defs (\exists \Delta Region @ PromoteRegion \land RegionAddBundleOk) \\ |
| \end{zed} |
| |
| This operation has the signature below, which shows that it is now an operation on the |
| system of multiple regions. |
| %%unchecked |
| \begin{schema}{RegionsAddBundleOk} |
| \Delta Regions \\ |
| rid? : RId \\ |
| b? : Bundle \\ |
| \where |
| \ldots |
| \end{schema} |
| |
| %============================================================================= |
| \clearpage |
| \section{Filters} |
| \label{cha:filters} |
| |
| So far the regions in the system are independent of each other. |
| When we later connect the regions together, we will need to define which bundles, |
| packages, and services are visible across each connection from one region to another. |
| We'll do this using a \textit{filter}. |
| |
| A filter specifies sets of bundles, packages, and services. |
| \begin{schema}{Filter} |
| bf : \power Bundle \\ |
| pf : \power Package \\ |
| sf : \power Service \\ |
| \end{schema} |
| |
| We define some helper functions to perform filtering. |
| |
| The $filterPackages$ function passes a set of exported packages through a filter. |
| \begin{axdef} |
| filterPackages : \power Package \cross Filter \fun \power Package \\ |
| \where |
| filterPackages = \{ ps : \power Package; f : Filter @ ((ps, f), ps \cap f.pf) \} |
| \end{axdef} |
| |
| The $filterServices$ function passes a set of published services through a filter. |
| \begin{axdef} |
| filterServices : \power Service \cross Filter \fun \power Service \\ |
| \where |
| filterServices = \{ ss : \power Service; f : Filter @ ((ss, f), ss \cap f.sf) \} |
| \end{axdef} |
| |
| The $bundleView$ function produces a filtered view of a bundle by applying a filter to the bundle's exported packages and published services. |
| \begin{axdef} |
| bundleView : Bundle \cross Filter \fun Bundle |
| \where |
| bundleView = (\lambda b: Bundle; f : Filter @ \\ |
| \t1 (\mu Bundle | \\ |
| \t2 location = b.location \land \\ |
| \t2 exportedPackages = filterPackages(b.exportedPackages, f) \land \\ |
| \t2 publishedServices = filterServices(b.publishedServices, f))) |
| \end{axdef} |
| |
| The $filterBundles$ function passes a set of bundles through a filter. |
| The result is the set of filtered views of the bundles allowed by the filter. |
| \begin{axdef} |
| filterBundles : \power Bundle \cross Filter \fun \power Bundle \\ |
| \where |
| filterBundles = (\lambda bs : \power Bundle; f : Filter @ \{ b : bs \cap f.bf @ bundleView(b, f) \}) \\ |
| \end{axdef} |
| |
| We also define the most permissive filter. |
| \begin{axdef} |
| TOP : Filter |
| \where |
| TOP.bf = Bundle \\ |
| TOP.pf = Package \\ |
| TOP.sf = Service \\ |
| \end{axdef} |
| |
| \subsection{Filtering Regions} |
| |
| %%inop \downarrow 6 |
| We define an infix operator $\downarrow$ to apply a filter to a region and produce another region. |
| \begin{axdef} |
| \_ \downarrow \_ : Region \cross Filter \fun Region \\ |
| \where |
| (\_ \downarrow \_) = (\lambda r : Region; f : Filter @ \\ |
| \t3 (\mu Region | \\ |
| \t4 bundles = filterBundles(r.bundles, f) \land \\ |
| \t4 pkg = filterPackages(r.pkg, f) \land \\ |
| \t4 svc = filterServices(r.svc, f))) \\ |
| \end{axdef} |
| $\downarrow$ is total since packages and services not filtered out which are exported or published by a |
| bundle which \textit{is} filtered out end up |
| in the resultant region's imported packages and imported services sets, respectively. |
| |
| The most permissive filter can be applied to any region without effect. |
| \begin{argue} |
| \shows \forall r : Region @ r \downarrow TOP = r \\ |
| \end{argue} |
| |
| Filters can be applied in any order with the same effect. |
| \begin{argue} |
| \shows \forall r : Region; f, g : Filter @ (r \downarrow f) \downarrow g = (r \downarrow g) \downarrow f \\ |
| \end{argue} |
| |
| $\downarrow$ distributes over $\sqcup$ (where defined). |
| \begin{argue} |
| \shows \forall f : Filter; r, s : Region | (r, s) \in ConsistentRegionPairs @ \\ |
| \t1 (r \downarrow f, s \downarrow f) \in ConsistentRegionPairs \land \\ |
| \t1(r \sqcup s) \downarrow f= (r \downarrow f) \sqcup (s \downarrow f) \\ |
| \end{argue} |
| |
| %============================================================================= |
| \clearpage |
| \section{Connected Regions} |
| \label{cha:connregions} |
| |
| We now connect up regions to form a directed graph. |
| |
| Certain pairs of distinct regions are connected by filters. The net effect of connecting a region to other |
| regions is that the region may then be able to see bundles, exported packages, and services in other regions. |
| This net effect is modelled as a collection of textit{net} regions. |
| |
| Every region can be considered to be connected to itself by the most permissive filter. |
| So the bundles in a region can see all the bundles, exported packages, and services in that region. |
| \begin{schema}{RegionDigraph} |
| Regions \\ |
| filter : RId \cross RId \pfun Filter \\ |
| net : RId \pfun Region \\ |
| \where |
| \dom filter \subseteq (rids \cross rids) \setminus \id RId \\ |
| \dom net = rids \\ |
| (\forall rid : rids @ \\ |
| \t1 net~rid = (reg~rid) \sqcup \bigsqcup \{ r : RId | (rid, r) \in \dom filter @ (net~r) \downarrow filter(rid, r)\})\\ |
| \end{schema} |
| |
| The $net$ function is well defined but this isn't immediately obvious. |
| Since there are finitely many regions, the $\bigsqcup$ expression in the constraint is well defined. |
| Also, we need to be sure that there is a $net$ function which satisfies the constraint. |
| This turns out to be the case because if we start at a given region $r$ and then form all the non-looping |
| paths to other regions, then we can apply all the filters along each non-looping path and then |
| use $\bigsqcup$ to combine the results to form $net~r$ observing that visiting the same region via |
| a longer, looping path does not affect the result since more filters will |
| be applied compared to the non-looping path to that region. |
| |
| \subsection{Connecting Regions Together} |
| |
| We define an operation to connect two distinct regions with a filter. |
| \begin{schema}{ConnectOk} |
| \Delta RegionDigraph \\ |
| r?, s? : RId \\ |
| f? : Filter \\ |
| \where |
| r? \neq s? \\ |
| (r?, s?) \notin \dom filter \\ |
| \theta Regions' = \theta Regions \\ |
| filter' = filter \cup \{ (r?, s?) \mapsto f? \} \\ |
| \end{schema} |
| |
| \subsection{Adding a Bundle to a Region} |
| |
| Adding a bundle to a region in the directed graph adds the bundle to a region in the |
| system of multiple regions and affects no connections or filters. |
| We add a constraint that the bundle being added must not |
| be present in a filter associated with the region the bundle is being added to. |
| This is to avoid a bundle in a region clashing with a bundle from a connected region. |
| \begin{schema}{CRAddBundleOk} |
| \Delta RegionDigraph \\ |
| RegionsAddBundleOk \\ |
| \where |
| filter' = filter \\ |
| (\forall s : RId; f : Filter | (rid?, s) \mapsto f \in filter @ \\ |
| \t1 b? \notin f.bf) \\ |
| \end{schema} |
| |
| \subsection{Determining a Bundle's Region} |
| |
| A bundle's region in the directed graph is the same as the bundle's |
| region in the syste, of multiple bundles. |
| This operation does not affect any connections or filters. |
| \begin{zed} |
| CRGetRegionOk \defs \Xi RegionDigraph \land GetRegionOk \\ |
| \end{zed} |
| |
| %============================================================================= |
| \clearpage |
| \section{Framework Hooks} |
| \label{cha:fhooks} |
| |
| We can now describe the behaviour of framework hooks in terms of our directed graph of regions. |
| |
| A bundle `find' operation, such as \texttt{BundleContext.getBundles}, is returned only the |
| candidates in the net region of the bundle performing the operation. |
| |
| That is, the bundle performing a bundle `find' operation is returned the bundles in its own region |
| and bundles in connected regions that are allowed by the corresponding filters. |
| \begin{schema}{BundleFindHook} |
| \Xi RegionDigraph \\ |
| finder? : Bundle \\ |
| candidates? : \power Bundle \\ |
| found! : \power Bundle \\ |
| \where |
| finder? \in allBundles \\ |
| found! = candidates? \cap (net(breg~finder?.location)).bundles \\ |
| \end{schema} |
| |
| A bundle listener receives only events for bundles in the net region of the bundle that was used |
| to register the listener. |
| |
| That is, the bundle listener receives events for bundles in the region used to register the listener |
| and for bundles in connected regions that are allowed by the corresponding filters. |
| \begin{schema}{BundleEventHook} |
| \Xi RegionDigraph \\ |
| listeners? : \power Bundle \\ |
| eb? : Bundle \\ |
| fl! : \power Bundle \\ |
| \where |
| listeners? \subseteq allBundles \\ |
| fl! = \{ l : listeners? | eb? \in (net(breg~l.location)).bundles \} \\ |
| \end{schema} |
| |
| A bundle being resolved may wire only to exported packages and bundles in the net region of the |
| bundle. |
| |
| That is, the bundle may wire to exported packages and bundles in its own region and to |
| exported packages and bundles in connected regions that are allowed by the corresponding filters. |
| \begin{schema}{ResolverHookFilterMatches} |
| \Xi RegionDigraph \\ |
| requirer? : Bundle \\ |
| candidates? : \power Package \\ |
| filtered! : \power Package \\ |
| \where |
| requirer? \in allBundles \\ |
| filtered! = candidates? \cap (net(breg~requirer?.location)).pkg \\ |
| \end{schema} |
| |
| A service `find' operation is returned only the |
| candidates in the net region of the bundle performing the operation. |
| |
| That is, the bundle performing a service `find' operation is returned the services in its own region |
| and services in connected regions that are allowed by the corresponding filters. |
| \begin{schema}{ServiceFindHook} |
| \Xi RegionDigraph \\ |
| finder? : Bundle \\ |
| candidates? : \power Service \\ |
| found! : \power Service \\ |
| \where |
| finder? \in allBundles \\ |
| found! = candidates? \cap (net(breg~finder?.location)).svc \\ |
| \end{schema} |
| |
| A service listener receives only events for services in the net region of the bundle that was used |
| to register the listener. |
| |
| That is, the service listener receives events for services in the region used to register the listener |
| and for services in connected regions that are allowed by the corresponding filters. |
| \begin{schema}{ServiceEventHook} |
| \Xi RegionDigraph \\ |
| listeners? : \power Bundle \\ |
| es? : Service \\ |
| fl! : \power Bundle \\ |
| \where |
| listeners? \subseteq allBundles \\ |
| fl! = \{ l : listeners? | es? \in (net(breg~l.location)).svc \} \\ |
| \end{schema} |
| |
| %============================================================================= |
| \newpage |
| \section{Z Notation} |
| \label{cha:znot} |
| |
| \makeatletter % the following code is taken from Mike Spivey's zed.tex |
| |
| \def\symtab{\setbox0=\vbox\bgroup \def\\{\cr} |
| \halign\bgroup\strut$##$\hfil&\quad##\hfil\cr} |
| \def\endsymtab{\crcr\egroup\egroup |
| \dimen0=\ht0 \divide\dimen0 by2 \advance\dimen0 by\ht\strutbox |
| \splittopskip=\ht\strutbox \vbadness=10000 |
| \predisplaypenalty=0 |
| $$\halign{##\cr\hbox to\linewidth{% |
| \valign{##\vfil\cr |
| \setbox1=\vsplit0 to\dimen0 \unvbox1\cr |
| \noalign{\hfil}\unvbox0\cr |
| \noalign{\hfil}}}\cr |
| \noalign{\prevdepth=\dp\strutbox}}$$ |
| \global\@ignoretrue} |
| |
| \makeatother |
| |
| Numbers: |
| \begin{symtab} |
| \nat & \verb/Natural numbers/ \{\verb/0,1,.../\} \\ |
| % \num & \verb/Integers (...,-1,0,1,...)/ \\ |
| % \nat_1 & \verb/Positive natural numbers/ \\ |
| % \upto & \verb/integral range/ \\ |
| % + & \verb/Addition/\quad\hfill 3 \\ |
| % - & \verb/Subtraction/\quad\hfill 3 \\ |
| % * & \verb/Multiply/\quad\hfill 4 \\ |
| % \div & \verb/Remainder/\quad\hfill 4 \\ |
| % \mod & \verb/Modulus/\quad\hfill 4 \\ |
| % < & \verb/Less than/ \\ |
| % > & \verb/Greater than/ \\ |
| % \leq & \verb/Less than or equal/ \\ |
| % \geq & \verb/Greater than or equal/ \\ |
| % \neq & \verb/Inequality/ \\ |
| \end{symtab} |
| Propositional logic and the schema calculus: |
| \begin{symtab} |
| % \lnot & \verb/Not/ \\ |
| \ldots\land\ldots & \verb/And/ \\ |
| \ldots\lor\ldots & \verb/Or/ \\ |
| \ldots\implies\ldots & \verb/Implies/ \\ |
| % \iff & \verb/If and only if/ \\ |
| \forall..\mid..\spot.. & \verb/For all/ \\ |
| \exists..\mid..\spot.. & \verb/There exists/ \\ |
| % \exists_1..\mid..\spot.. & \verb/There exists unique/ \\ |
| \ldots\hide\ldots & \verb/Hiding/ \\ |
| % \project & \verb/\project/ \\ |
| % \pre & \verb/\pre/ \\ |
| % \semi & \verb/\semi/ |
| \ldots\defs\ldots & \verb/Schema definition/ \\ |
| \ldots==\ldots & \verb/Abbreviation/ \\ |
| \ldots::=\ldots\mid\ldots & \verb/Free type definition/ \\ |
| \ldata\ldots\rdata & \verb/Free type injection/ \\ |
| [\ldots] & \verb/Given sets/ \\ |
| ',?,!,_0\ldots_9 & \verb/Schema decorations/ \\ |
| \ldots\shows\ldots & \verb/theorem/ \\ |
| \theta\ldots & \verb/Binding formation/ \\ |
| \lambda\ldots & \verb/Function definition/ \\ |
| \mu\ldots & \verb/Mu-expression/ \\ |
| \Delta\ldots & \verb/State change/ \\ |
| \Xi\ldots & \verb/Invariant state change/ \\ |
| \end{symtab} |
| Sets and sequences: |
| %and bags: |
| \begin{symtab} |
| \{\ldots\} & \verb/Set/ \\ |
| \{..\mid..\spot..\} & \verb/Set comprehension/ \\ |
| \power\ldots & \verb/Set of subsets of/ \\ |
| % \power_1 & \verb/Non-empty subsets of/ \\ |
| % \finset & \verb/Finite sets/ \\ |
| % \finset_1 & \verb/Non-empty finite sets/ \\ |
| \emptyset & \verb/Empty set/ \\ |
| \ldots\cross\ldots & \verb/Cartesian product/ \\ |
| \ldots\in\ldots & \verb/Set membership/ \\ |
| \ldots\notin\ldots & \verb/Set non-membership/ \\ |
| \ldots\cup\ldots & \verb/Union/ \\ |
| \ldots\cap\ldots & \verb/Intersection/ \\ |
| \ldots\setminus\ldots & \verb/Set difference/ \\ |
| \bigcup\ldots & \verb/Distributed union/ \\ |
| % \bigcap & \verb/Distributed intersection/ \\ |
| \#\ldots & \verb/Cardinality/ \\ |
| % \dcat & \verb/Distributed sequence concatenation/ |
| \ldots\subseteq\ldots & \verb/Subset/ \\ |
| \ldots\subset\ldots & \verb/Proper subset/ \\ |
| \ldots\partition\ldots & \verb/Set partition/ \\ |
| \seq & \verb/Sequences/ \\ |
| % \seq_1 & \verb/Non-empty sequences/ \\ |
| % \iseq & \verb/Injective sequences/ \\ |
| \langle\ldots\rangle & \verb/Sequence/ \\ |
| % \cat & \verb/Sequence concatenation/ \\ |
| \disjoint\ldots & \verb/Disjoint sequence of sets/ \\ |
| % \bag & \verb/Bags/ \\ |
| % \lbag\ldots\rbag & \verb/Bag/ \\ |
| % \inbag & \verb/Bag membership/ \\ |
| \end{symtab} |
| %Here are the infix function symbols. Each symbol is |
| %shown with its priority: |
| %\begin{symtab} |
| % \uplus & \verb/\uplus/ \\ |
| % \filter & \verb/Schema projection/ \\ |
| % \uminus & \verb/\uminus/ |
| %\end{symtab} |
| Functions and relations: |
| \begin{symtab} |
| \ldots\rel\ldots & \verb/Relation/ \\ |
| \ldots\pfun\ldots & \verb/Partial function/ \\ |
| \ldots\fun\ldots & \verb/Total function/ \\ |
| \ldots\pinj\ldots & \verb/Partial injection/ \\ |
| \ldots\inj\ldots & \verb/Injection/ \\ |
| % \psurj & \verb/Partial surjection/ \\ |
| % \surj & \verb/Surjection/ \\ |
| % \bij & \verb/Bijection/ \\ |
| % \ffun & \verb/Finite partial function/ \\ |
| % \finj & \verb/Finite partial injection/ \\ |
| \dom\ldots & \verb/Domain/ \\ |
| \ran\ldots & \verb/Range/ \\ |
| \ldots\mapsto\ldots & \verb/maplet/ \\ |
| \ldots\inv & \verb/Relational inverse/ \\ |
| % \ldots\plus & \verb/Transitive closure/ \\ |
| \ldots\star & \verb/Reflexive-transitive closure/ \\ |
| % \ldots\bsup n \esup & \verb/Relational iteration/ \\ |
| \ldots\limg\ldots\rimg & \verb/Relational image/ \\ |
| % \comp & \verb/Forward relational composition/ \\ |
| % \circ & \verb/Relational composition/ \\ |
| \ldots\oplus\ldots & \verb/Functional overriding/ \\ |
| \ldots\dres\ldots & \verb/Domain restriction/ \\ |
| % \ldots\rres\ldots & \verb/Range restriction/ \\ |
| \ldots\ndres\ldots & \verb/Domain subtraction/ \\ |
| % \ldots\nrres\ldots & \verb/Range subtraction/ \\ |
| % \id & \verb/Identity relation/ \\ |
| \end{symtab} |
| Axiomatic descriptions: |
| %%unchecked |
| \begin{axdef} |
| Declarations |
| \where |
| Predicates |
| \end{axdef} |
| Schema definitions: |
| %%unchecked |
| \begin{schema}{SchemaName} |
| Declaration |
| \where |
| Predicates |
| \end{schema} |
| \end{document} |