genevan
The genevan package provides a simple generic version negotiation algorithm.
Features
- Protocol-independent; the package provides version negotiation semantics without reference to any specific communications protocol.
- Formal specification with proofs of correctness of various properties of the protocol.
- Written in pure Java 21.
- High coverage automated test suite.
- OSGi-ready.
- JPMS-ready.
- ISC license.
Informal Description
A server provides a list of protocol names, and each protocol name has a list
of supported version numbers. Call this list ssp.
A client provides a list of protocol names, and each protocol name has a list
of supported version numbers. Call this list csp.
The server provides ssp to the client, and the client removes all of the
elements of ssp that do not appear in csp. The client then further filters
the list by removing all but the highest version numbers for each named
protocol. Call this filtered list cfsp.
If cfsp contains a single protocol name and version, the client sends this
protocol name and version to the server, the server confirms the selection,
and the client and server communicate using that version of that protocol
from that point onwards. The negotiation algorithm is completed.
If cfsp contains more than a single protocol name and version, the client
consults a possibly-empty list of preferred protocol names.
Call this list cpp. The first element of cpp that has the same name as
an element in csfp is selected, the client sends this protocol name and
version to the server, the server confirms the selection, and the client and
server communicate using that version of that protocol from that point onwards.
The negotiation algorithm is completed.
If no elements of cpp match any elements in cfsp, then the client and
server are in an ambiguous state: They both have multiple protocols and
versions in common, but there is no deterministic way to pick one;
communcation ends at this point with an error.
At any point, if the client tries to send a protocol name and version that the server does not support, communication ends at that point with an error.
Formal Description
A formal description of the protocol, including proofs of correctness, are provided in the given Coq development.
A protocol version consists of a pair of natural numbers representing the major and minor version of the protocol:
Inductive ProtoVersion := {
prMajor : nat;
prMinor : nat
}.
A protocol name is a string.
Definition ProtoName := string.
A protocol identifier is the combination of a protocol name and version:
Inductive ProtoIdentifier := {
prName : ProtoName;
prVersion : ProtoVersion
}.
Protocol versions are totally ordered, with the order defined as the comparison between major versions, followed by the comparison between minor versions:
Definition protoVersionCmp (p0 p1 : ProtoVersion) : comparison :=
match Nat.compare (prMajor p0) (prMajor p1) with
| Eq => Nat.compare (prMinor p0) (prMinor p1)
| Lt => Lt
| Gt => Gt
end.
The maximum of two protocol versions x and y is defined accordingly:
Definition max (x y : ProtoVersion) : ProtoVersion :=
match protoVersionCmp x y with
| Eq => x
| Lt => y
| Gt => x
end.
The max function is reflexive, commutative, and associative. Accordingly,
given a non-empty list of protocol versions, the maximum of the list is
defined:
Fixpoint maxList
(xs : list ProtoVersion)
: option ProtoVersion :=
match xs with
| [] => None
| y :: ys =>
match maxList ys with
| None => Some y
| Some w => Some (max y w)
end
end.
An empty list has no maximum.
The server exposes a list of protocol identifiers. We need to compare the list of protocol identifiers held by the client with those held by the server. A protocol identifier is said to be supported by another protocol identifier if the name and major version match:
Definition isSupportedBy
(x y : ProtoIdentifier)
: Prop :=
(prName x) = (prName y) /\ (prMajor (prVersion x) = prMajor (prVersion y)).
The isSupportedBy relation is reflexive, transitive, and symmetric (it
is an equivalence relation). It is also decidable, as equality of names and
version numbers is decidable.
The result of attempting to negotiate a protocol is either success or failure, with failure cases being limited to ambiguity, or no suitable protocol being available.
Inductive Error :=
| ErrorNoSolution
| ErrorAmbiguous : list ProtoIdentifier -> Error.
Inductive Result (A : Set) : Set :=
| Success : A -> Result A
| Failure : Error -> Result A.
Given a list of protocols supported on the server side, and a list of protocols supported on the client side, we first remove all unsupported protocols:
Definition bestVersionsOfAll
(identifiers : list ProtoIdentifier)
: list ProtoIdentifier :=
withoutOptions (bestVersionsOfAllOpt identifiers).
We can then pick a best protocol without any attempt made to avoid ambiguity:
Definition solveWithoutDisambiguation
(serverSupports : list ProtoIdentifier)
(clientSupports : list ProtoIdentifier)
: Result ProtoIdentifier :=
match withoutUnsupported serverSupports clientSupports with
| Failure _ f => Failure _ f
| Success _ supported =>
let bestVersions := bestVersionsOfAll supported in
match bestVersions with
| [] => Failure _ ErrorNoSolution
| [x] => Success _ x
| xs => Failure _ (ErrorAmbiguous xs)
end
end.
If the result is ambiguous, we then disambiguate by picking a protocol from a provided client-side list:
Fixpoint disambiguate
(xs : list ProtoIdentifier)
(preferences : list ProtoName)
: Result ProtoIdentifier :=
match preferences with
| [] => Failure _ (ErrorAmbiguous xs)
| p :: ps =>
match findWithName xs p with
| Some r => Success _ r
| None => disambiguate xs ps
end
end.
Definition solve
(serverSupports : list ProtoIdentifier)
(clientSupports : list ProtoIdentifier)
(preferences : list ProtoName)
: Result ProtoIdentifier :=
match solveWithoutDisambiguation serverSupports clientSupports with
| Success _ r => Success _ r
| Failure _ ErrorNoSolution => Failure _ ErrorNoSolution
| Failure _ (ErrorAmbiguous xs) => disambiguate xs preferences
end.
As mentioned, see the genevan.v development for the exact definitions of
all functions, and proofs of various properties of the protocol.
Usage
Create a protocol solver:
var solver =
GenProtocolSolver.create();
Supply the solver with the protocol names and versions that the server supports,
the protocol names and versions that the client supports, and a possibly-empty
list of protocol names that the client prefers. The solver will pick the
best protocol to send to the server, or it will throw an
GenProtocolException explaining why it could not pick:
Collection<? extends GenProtocolServerEndpointType> serverSupports;
Collection<? extends GenProtocolClientHandlerType> clientSupports;
List<String> preferProtocols;
var solved =
solver.solve(
serverSupports,
clientSupports,
preferProtocols
);
Releases & Development Snapshots
Releases
You can subscribe to the atom feed to be notified of project releases.
The most recently released version of the package is 1.0.0.
1.0.0 Release (2024-05-11Z)
The compiled artifacts for the release (and all previous releases) are available on Maven Central.
Maven Modules
<dependency> <group>com.io7m.genevan</group> <artifactId>com.io7m.genevan.core</artifactId> <version>1.0.0</version> </dependency><dependency> <group>com.io7m.genevan</group> <artifactId>com.io7m.genevan.tests</artifactId> <version>1.0.0</version> </dependency>
Development Snapshots
At the time of writing, the current unstable development version of the package is 1.0.1-SNAPSHOT.
Development snapshots may be available in the Central Portal Snapshots repository. Snapshots are published to this repository every time the project is built by the project's continuous integration system, but snapshots do expire after around ninety days and so may or may not be available depending on when a build of the package was last triggered.
Manual
This project does not have any user manuals or other documentation beyond what might be present on the page above.
Sources
This project uses Git to manage source code.
Repository: https://www.github.com/io7m-com/genevan
$ git clone --recursive https://www.github.com/io7m-com/genevan
Issues
This project uses GitHub Issues to track issues.
License
Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies. THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.