| JVM | Platform | Status |
|---|---|---|
| OpenJDK (Temurin) Current | Linux |  |
| OpenJDK (Temurin) LTS | Linux |  |
| OpenJDK (Temurin) Current | Windows |  |
| OpenJDK (Temurin) LTS | Windows |  |
The genevan package provides a simple generic version negotiation algorithm.
- 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.
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.
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.
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
);