We are concerned with two major classes of problems with large distributed systems; 1) bugs and operator errors that cause a departure from the logical intent o

We are concerned with two major classes of problems with large distributed systems; 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising 'sustained emergent performance degradation' of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. (...) A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. (...) TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don't yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. Interesting. TLA+ of course allows for hybrid specifications that incorporate physical constraints --real-time itself being the prime example--, so constraints based on more complicated 'loss functions' like, say, weighted average or total variation of response times, in principle ought to be feasible as well. Leslie Lamport himself laments such specifications are still 'of only academic interest' [1, §9.5], so I wonder how impractical such specifications could they really get. [1] http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...