WingNews logo WingNews
top | item 9476513

(no title)

excel2flow | 10 years ago

Could have abstract interpretation (http://www.astree.ens.fr/) or some other formal method prevented it?

discuss

order

tlb|10 years ago

Someone wrote something like:

  int32_t ticks; // 100ths of a second
which overflows in 248 days, a particularly unfortunate amount of time because it doesn't show up during testing.

Although it would be a good engineering choice, a formal verifier would say that:

  int64_t ticks; // 100ths of a second
is also incorrect, since it also overflows (after 10^9 years).

In a hard real time system,

  mpz_t ticks; // 100ths of a second, infinite precision libgmp type
is still formally incorrect, since as the the number grows in size it will eventually exceed a time limit or memory (after 10^10^9 years)

The overall lesson from formal methods is that it's impossibly to write formally correct useful programs. So programmers just muddle through.

cnvogel|10 years ago

As you have written, a formal test/analysis will always detect that a monotonously increased tick counter will not be bound by an upper limit. And the obvious solution is that you don't rely on such a thing, but define your API such that the (preferably unsigned, but doen't matter) tick-counter will roll over in a well defined way.

If the algorithms really depend on an always monotonously increasing tick-counter (which I doubt), the solution is quite easy: After 2^30 ticks set a flag which raises the "service needed" light in the cockpit, taking the plane out of service until it's power cycled. By this you explicitly state that your device cannot be used longer than 120 days continuously.

ambrop7|10 years ago

A general solution to the overflowing-clock problem is to deal with the clock in modular arithmetic. When wanting to know if t2 comes before t1, check the MSB of the modular difference.

  uint32_t t1 = ...;
  uint32_t t2 = ...;
  if ((uint32_t)(t2 - t1) >= UINT32_C(0x80000000)) {
    // t2 is before t1
  } else {
    // t2 is after or equal to t1
  }
What this gives us is that if the difference of the actual times (not these uint32 representations which are ambiguous modulo 2^32) is less than 2^31 units (plus minus one maybe..), this check will give the expected result. This does allow a correct system that never fails if the timing/duration of the events is suitably limited.

For example you time events at a fixed time interval, and it will keep going forever in spite of clock roll-over.

  uint32_t next_time = now();
  while (1) {
    while ((uint32_t)(now() - next_time) >= UINT32_C(0x80000000));
    printf("Shoot\n");
    next_time += interval;
  }
The timing events also need to be processed quickly enough of course (that printf shouldn't block for longer than about 2^31).

tgbrter|10 years ago

I disagree. You can reduce space usage with a logarithmic complexity. A couple tens of bytes is enough to store miliseconds until the heat death of the universe.

mhogomchungu|10 years ago

> int64_t ticks; // 100ths of a second

I would go with uint64_t

as it documents "ticks" as a variable that can not hold negative values and also doubles its range of positive values.

CamperBob2|10 years ago

Another good practice is to initialize the time counters to something close to the overflow point, rather than zero. This encourages overflow bugs to show up at timescales where they will be noticed during testing, rather than after 248 days of service.

This is a scary-ass bug in a codebase that was supposed to be authored to strict professional standards.