Consolidation

[jklmnn]

The current project has seen many architectural changes, especially on Linux. The current state, while it works for the tests is still in the state of a proof of concept and does likely contain errors. This is especially true for

• file descriptor leaks, especially in error handling code
• unproved message generation code
• handling of unexpected file descriptor closes (although we do not have defined a policy how components should behave)
• unprovable constructs in session interfaces

Furthermore the next version will also bring a high number of changes, including new interfaces and a new platform/kernel. I see two possibilities:

• Let the current and the next version as is and insert a dedicated consolidation version after the next one. This reduces the time used for proofs as it avoids proving code that is going to be changed anyway. But it has the risk that we end up with a result that is hard/impossible to proof and that the proofs have to be redone.
• Make an 80% proof of the Linux broker and a 100% proof of the test cases now. This validates the design of the current interfaces and removes the most problematic errors from the broker. However it induces the risk that the we have to redo much of this if we need to make an architectural change in the next version.

The same applies to the file descriptor problematic. Since this is a Linux only problem it would only be affected if we'd do an architectural change. I see two possibilities here:

• Fix it now with a medium risk to introduce new problems if we do architectural changes.
• Annotate problematic parts but fix them after the next version. This has the advantage that we do not forget problematic parts but that it is relatively low effort and that it can be adapted to changes with virtually no effort.

We also have to take into consideration that fixing file descriptor leaks and proving the broker will affect each other, especially as it touches global state.

[jklmnn]

Discussion result:

• prove tests and interfaces to show that interfaces can be proven
• prove broker 80%
• mark file descriptor leaks and fix them by hand
  • 2nd step: create a reference counted wrapper for file descriptors that allows to prove that no leaks are existent