Generally for more complex systems, an improbable failure mode becomes a certitude.
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.
That's a bit different, isn't it? As agda is total, and requires everything be proved to halt. Whereas the context here is a complete language, where you do not get such strong properties, but must still try to reason anyway. I didn't discuss any specific ways to infer termination or nontermination (though I definitely think those are interesting too!), only a broad strategy for reasoning about them.
> As agda is total, and requires everything be proved to halt.
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
It's trivial to write any program using Delay, e.g. if we have a function 'step: TuringMachine -> TuringMachine' which performs one step of any Turing machine, we can run any TuringMachine using:
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
This is similar to "infinite lists" in lazy languages (like Haskell); e.g. if we call 'run' with a non-halting TuringMachine, we'll get 'Later (Later (Later (...)))'
But I mean, 'run' is a total function and it does halt. When you call 'run' on your non-halting TuringMachine, the language interpreter reduces exactly one call to 'step' and then terminates with the result 'Later <an unevaluated expression>'. Further computation only occurs if and when you pump the 'Later ...' value for further terms, and that can happen only finitely many times because repeated pumping can only come from a standard recursion, ultimately, which is terminating.
Oops, yeah; I know Agda needs special handling for codata (co-patterns, sharp/flat, etc.)
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.)
GCC does take advantage of the forward progress guarantee in other cases, but seemingly only in c++ mode; see https://godbolt.org/z/Won5zETKx. I wonder why.
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.
16 comments
[ 3.1 ms ] story [ 51.4 ms ] threadIn 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:
It's trivial to write any program using Delay, e.g. if we have a function 'step: TuringMachine -> TuringMachine' which performs one step of any Turing machine, we can run any TuringMachine using: This is similar to "infinite lists" in lazy languages (like Haskell); e.g. if we call 'run' with a non-halting TuringMachine, we'll get 'Later (Later (Later (...)))'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...
[2]: https://godbolt.org/z/5Yj8K5vzr
[3]: https://godbolt.org/z/M6vq5KKnj
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.