eport from the 20160501 F2

[Daniel Franke]

Resent copying the list this time.

On 5/3/16, Hal Murray <hmurray at megapathdsl.net> wrote:
>
>> A from-scratch proven and verified C implementation of "simple NTP
>> broadcast
>> client" will be written.  Lead on that project will be Daniel.
>
> Could you say a bit more?  How "simple"?  What does "verified" mean?

For the initial version: no configuration at all. Listens for NTP
broadcast packets on UDP port 123, computes offsets, calls adjtime(),
loops. Later I might add support for sending an initial volley to a
server given on the command line. Verify, probably using VST but maybe
Verifast or Frama-C, that the program has no undefined behavior and
will never hang or crash. Possibly prove additional correctness
properties if I can manage to specify them in a way such that the
correctness of the specification is more obvious to me than the
correctness of the implementation.

> What are you expecting in the way of timekeeping accuracy and/or glitch
> avoidance?  Is there a target audience?  Are you expecting it to work
 >(well)
> on WiFi as well as Ethernet?

The primary target audience is IoT devices. Expect nothing impressive
in terms of timekeeping precision.

>> The diag dump "nameless horror" shall be removed from NTPsec.
>
> What is that?  I don't recognize the term.

Support for the ntpq saveconfig command. The term is a joke from the
meeting because it took five minutes before any of us could remember
what it was called.