Coping with nontermination: some thoughts on stopping loops
outerproduct.net
outerproduct.net
In general, in C/C++ one needs to accept many popular libraries slowly leak memory, bad design fragments memory, and thread-safe is often not the norm. However, for long running tasks there are several methods to mitigate the problems.
1. Add a watchdog-timer thread that garbage collects its peer even in a single process thread-unsafe program. The design requires every thread has a sleeping watchdog-timer monitor peer with a shared structure containing a mutex, peer thread ID, counter variable, periodic polling sleep interval, and error message handler. This means for n threads, there will always be 2*n +1 threads allocated, and n+1 sleeping most of the cycles (low lock contention). The watchdog timer is reset before entering a loop, or key data access/mutation operations. i.e. if there is a cycle formed in the thread(s) that locks up, than >1 watchdog timer threads is guaranteed to trip the timeout event as it breaks the expected run-time limit.
2. set transaction call quota limits, and cleanly restart a new instance of a program at regular intervals. Even with ECC ram this is highly recommended.
3. external queuing pattern with transaction confirmation, timeouts, thumb-printing, and GUID. i.e. when data is corrupted/hanged, the system redirects the task to an error handler/counter.
Happy computing, =)
https://agda.readthedocs.io/en/v2.6.0.1/language/termination...
Not quite; everything in Agda must either terminate or co-terminate. We can use co-termination to represent general recursion, e.g. using Delay:
data Delay : Type -> Type where
Now : {t: Type} -> t -> Delay t
Later : {t: Type} -> Delay t -> Delay t
run : TuringMachine -> Delay TuringMachine
run thisState = case thisState == nextState of
true -> Now thisState -- We've entered a halting state
false -> Later (run nextState)
where nextState = step thisState
Ironically, I'm more familiar with using codata in Coq; even though it's notoriously under-supported (breaking subject-reduction, no alternative to cofix, etc.)
Yes, 'Delay t' stores a value "at the end" (in the 'Now' constructor), but doesn't store anything "on the way" (in the 'Later' constructor).
In contrast, 'List t' stores values "on the way" (in Cons), but doesn't store anything "at the end" (in Nil).
Another useful example is (Peano) natural numbers, which don't store any values "at the end" (Zero) or "on the way" (Successor).
Natural numbers are isomorphic to 'List ()' and 'Delay ()' (whose 'elements' contain no information)
> Lists have a consumable head
Slight nit-pick: only non-empty lists have a head. Non-empty lists are isomorphic to '(t, List t)'.
Consuming the head of a 'Delay t' is still useful, since they act like a counter; or (equivalently) as a notion of logical time.
I find this stuff fascinating, and explored it in more detail at http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.htm...
i = 0;
while (i != 1)
i ^= 2;
return i;
.L2:
b .L2
mov w0, #1
ret
C provides forward progress guarantees only for loops, whereas C++ provides them for all code. Perhaps GCC did not want to bother to annotate individual control edges (as llvm does with 'mustprogress'), and they perform such optimisations after canonicalising loops and other irregular mechanisms for control flow into a homogenous CFG.