Rigorous definition of semantic compatibility and bit compatibility

[pavel-kirienko]

So I was writing the new spec doc and got stuck at the semantic and binary compatibility part. I'm leaving the lab right now with the intention of getting back to this first thing in the morning. @kjetilkjeka if you happened to have good definitions at hand, please share here.

This is what I ended up drafting so far:

\section{Data type compatibility and versioning}\label{sec:dsdl_versioning}

\subsection{Rationale}

As can be seen from the preceding sections,
the concept of \emph{data type} is a cornerstone feature of UAVCAN,
which sets it apart from many competing solutions.

In order to be able to interoperate successfully,
all nodes connected to the same bus must use compatible definitions of all employed data types.
This section is dedicated to the concepts of \emph{data type compatibility}
and \emph{data type versioning}.

A \emph{data type} is a named set of data structures defined in DSDL.
As has been explained above, in the case of message data types,
the set consists of just one data structure, whereas in the case of service data types
the set is a pair of request and response data structures.

Data type definitions may evolve over time as they are refined to better address the needs of their applications.
In order to formalize the data type evolution process with respect to the data type compatibility concerns,
UAVCAN introduces two concepts: \emph{semantic compatibility} and \emph{binary compatibility},
which are discussed below.

\subsection{Semantic compatibility}

\subsection{Binary compatibility}

[kjetilkjeka]

I think that compatibility is about the set of features being a subset/superset of some other set of features.

I think binary compatibility is the least difficult. Perhaps binary compatibility can be defined as something in the lines of the following.

We say that a definition (the compatible definition) is binary backwards compatible with another definition (the original defintion) if all the following statements hold:

• Every non void field in the original data type must also exist for the compatible data type. (A field with the exact same name, type and position in regards to serialization must exist).
• For every non-void field that exists in the compatible definition that do not exist in the original definition there must be a void field in the original definition encapsulating (in regards to serialization) the whole new non-void field.

Semantic compatibility is more tricky. I have summed up a few properties i think we need to have without attempting to write a formal definition.

• When adding a new const, there must be a sensible default that the old definition may use (For instance adding new error types is Ok, since every value besides the OK value must be treated as an unknown error)
• When adding new fields the void field serialization 0 must make sense.
  • For a status field 0 must be the equivalent to "nothing to report".
  • For a value field there are several hacks. 0 can mean "no value" or if the value 0 is needed one of the bits of the void field can be used as a "value exists" bit.
• When adding a new field existing fields must not change their behaviour based on values from the new field. However, the new field may change behaviour based on existing fields.

Compatibility aside, we should also avoid changes where the following is likely to occur:

• Users will be surprised by the changes.
• It will break stuff.

And at last:

• "We say that a definition is backwards compatible with another definition if it is both semantic and binary compatible with this definition.
• We say that a definition is backwards compatible If it is backwards compatible with all definitions sharing the same major version number and have smaller minor version number"

[pavel-kirienko]

Look, that seems unnecessarily strict and overdefined. Allow me to provide a counterexample (it's actually not made up, it's something I've been dealing with not so long ago). Here's definition A:

# Alert flags are allocated at the bottom (from bit 0 upwards)
uint64 DC_UNDERVOLTAGE                       = 1 << 0
uint64 DC_OVERVOLTAGE                        = 1 << 1
uint64 DC_UNDERCURRENT                       = 1 << 2
uint64 DC_OVERCURRENT                        = 1 << 3
uint64 CPU_COLD                              = 1 << 4
uint64 CPU_OVERHEATING                       = 1 << 5
uint64 VSI_COLD                              = 1 << 6
uint64 VSI_OVERHEATING                       = 1 << 7
uint64 MOTOR_COLD                            = 1 << 8
uint64 MOTOR_OVERHEATING                     = 1 << 9
uint64 HARDWARE_LVPS_MALFUNCTION             = 1 << 10
uint64 HARDWARE_FAULT                        = 1 << 11
uint64 HARDWARE_OVERLOAD                     = 1 << 12
uint64 PHASE_CURRENT_MEASUREMENT_MALFUNCTION = 1 << 13

# Non-error flags are allocated at the top (from bit 63 downwards)
uint64 UAVCAN_NODE_UP                        = 1 << 56
uint64 CAN_DATA_LINK_UP                      = 1 << 57
uint64 USB_CONNECTED                         = 1 << 58
uint64 USB_POWER_SUPPLIED                    = 1 << 59
uint64 RCPWM_SIGNAL_DETECTED                 = 1 << 60
uint64 PHASE_CURRENT_AGC_HIGH_GAIN_SELECTED  = 1 << 61
uint64 VSI_MODULATING                        = 1 << 62
uint64 VSI_ENABLED                           = 1 << 63

# Status flags, see the constants above
uint64 flags

Here's definition B. Its constants and fields differ from the previous definition, yet it is fully compatible:

# Alert flags are allocated at the bottom (from bit 0 upwards)
uint32 ALERT_DC_UNDERVOLTAGE                       = 1 << 0
uint32 ALERT_DC_OVERVOLTAGE                        = 1 << 1
uint32 ALERT_DC_UNDERCURRENT                       = 1 << 2
uint32 ALERT_DC_OVERCURRENT                        = 1 << 3
uint32 ALERT_CPU_COLD                              = 1 << 4
uint32 ALERT_CPU_OVERHEATING                       = 1 << 5
uint32 ALERT_VSI_COLD                              = 1 << 6
uint32 ALERT_VSI_OVERHEATING                       = 1 << 7
uint32 ALERT_MOTOR_COLD                            = 1 << 8
uint32 ALERT_MOTOR_OVERHEATING                     = 1 << 9
uint32 ALERT_HARDWARE_LVPS_MALFUNCTION             = 1 << 10
uint32 ALERT_HARDWARE_FAULT                        = 1 << 11
uint32 ALERT_HARDWARE_OVERLOAD                     = 1 << 12
uint32 ALERT_PHASE_CURRENT_MEASUREMENT_MALFUNCTION = 1 << 13
uint32 alert_flags

uint32 STATUS_UAVCAN_NODE_UP                       = 1 << 24
uint32 STATUS_CAN_DATA_LINK_UP                     = 1 << 25
uint32 STATUS_USB_CONNECTED                        = 1 << 26
uint32 STATUS_USB_POWER_SUPPLIED                   = 1 << 27
uint32 STATUS_RCPWM_SIGNAL_DETECTED                = 1 << 28
uint32 STATUS_PHASE_CURRENT_AGC_HIGH_GAIN_SELECTED = 1 << 29
uint32 STATUS_VSI_MODULATING                       = 1 << 30
uint32 STATUS_VSI_ENABLED                          = 1 << 31
uint32 status_flags

Needless to say, similar examples can be easily produced with void fields as well, and even with differently typed and differently sized dynamic arrays. Therefore I would avoid talking about fields and constants completely.

I propose a relaxed definition of bit (binary) compatibility: a structure definition A is bit-compatible with a structure definition B if any valid encoded representation of B is also a valid encoded representation of A (better wording highly welcome). Observe that this property is not commutative: it guarantees that what can be parsed by B can also be parsed by A, but the reverse may not be true (e.g. in the case of differently typed dynamic arrays). We are going to require mutual compatibility within the same major version: both A -> B and B -> A.

The above says nothing about semantics. The semantic compatibility can be defined in terms of application behavior: a structure definition A is semantically compatible with a structure definition B if an application that correctly uses A behaves identically to an application that correctly uses B. I'm going to refine the wording, right now we should be focused on the concept only.

Does that make sense? Note that your compatibility checking tool may use stricter, less generic compatibility checks. As I said before, checking semantic compatibliity as defined here is impossible unless the tool can reason about the application and understand the problem domain.

[kjetilkjeka]

Ok, so binary compatibility is only about serialization. That makes sense. My definition mixed in what applications can expect as well. My proposed constraints will implicitly enforce both the bit compatibility constraints and some other constraints. But it may still be valuable to have a clear split between them.

Your example is then indeed binary compatible. But if one attempted to update the definition in an application the new code would not compile. And due to that I would say that definition B should not be considered compatible (in the sense of "total compatibility") with definition A. I see two simple ways to keep them compatible.

1. Instead of changing types introduce bitmasks uint64 STATUS_FLAG_BM = 0xffffffff00000000
2. Introduce a concept of untagged unions in dsdl (this might very well be undesired as it makes things a bit more weird and may be difficult to support for some languages).

I think I described the least strict sensible definition for bit/binary/serialization compatibility in OpenCyphal-Garage/uavcan.github.io#40 there's no good precise definition there but it can perhaps be used for inspiration? To sum it up, all it cares about are the layout of static fields vs dynamic fields vs union fields.

[pavel-kirienko]

Closing for #6