The TLA
research.microsoft.com
research.microsoft.com
http://research.microsoft.com/en-us/um/people/lamport/tla/tl...
"TLA stands for the Temporal Logic of Actions, but it has become a shorthand for referring to the TLA+ specification language and the PlusCal algorithm language, together with their associated tools."
"TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems."
and
http://research.microsoft.com/pubs/64074/lamport-actions.pdf
"The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician’s toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere."
It's a programming language?
There are examples of using this to prove correctness of distributed algorithms such as Paxos:
http://research.microsoft.com/en-us/um/people/lamport/tla/by... http://research.microsoft.com/en-us/um/people/lamport/tla/Co...
This page can be found by searching the Web for the 21-letter string {redacted}. Please do not put this string in any document that could wind up on the web--including email messages and pdf and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamporttlahomepage".
Google's first result for "microsoft tla homepage" is this article, as is DDG's, so the unique keyword is of dubious value. As you say, a unique URL is more useful, because it's guaranteed to be unique.
Interestingly, if you search instead for "lamport tla homepage" (which is semantically easier than "uid-lamporttlahomepage and subtract the hyphen"), google gives you the same result, whereas DDG gives you the same link, but now it's called Lamport's TLA Homepage instead of The TLA Home Page.
There was such a huge disconnect between the world views and educational backgrounds of a team of systems programmers and the world of formal proofs. All exacerbated by TLA+ using logic notation more common in Britain than America...
In case you were hoping for info about TLA under jrockit, here's a starter read on that: http://docs.oracle.com/cd/E13150_01/jrockit_jvm/jrockit/geni...
This appears not the same as ThreadLocal classes of objects in Java. It has more to do with heap allocations for improving performance of object allocation. I think more like a segment of heap allocated per thread for quick object allocations, so that there is no need to coordinate a free block from the larger heap (likely to be slower).