The TLA(research.microsoft.com)
research.microsoft.com
The TLA
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html
6 comments
None of that helps me understand what it is.
It's a programming language?
It's a programming language?
From a brief overview of the paper, TLA is a language for proving "good" and "bad" properties for an abstract system. For instance, you can use it to prove that an algorithm completes within N seconds, or that an algorithm never reaches a certain unsafe state.
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...
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...
Interesting idea displayed at the bottom of the page. Note that I've removed the key string and replaced it with {redacted}. Ultimately, though, I can imagine a scheme like this wouldn't work very well in general use - that is why we have unique URLs.:
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".
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".
In the 90s and early noughties it was common for websites to have a paragraph at the bottom of the page containing nothing but keywords for search engines. Usually it was in small print or made to be casually invisible, but the keyword idea is one of the first things people did to get search engines targetting them... and search engines don't like keywords since people were using irrelevant once to catch traffic. Mind you, the layout of the page looks like it's from bang in the middle of the 'keyword' period... which is why it's strange to see it branded with 2013 and 2010.
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.
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.
Not to be confused with:
https://en.wikipedia.org/wiki/Three-letter_acronym
https://en.wikipedia.org/wiki/Three-letter_acronym
When I clicked on 'Click here to find out' I was expecting some self-referential joke.
One of the oddest experiences of my professional career was attending a day long "training session" where Leslie Lamport tried to teach a team of engineers how to use TLA+
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...
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...
I was pretty convinced this was going to be something about thread local area and jvm's, and totally confused by the microsoft domain. I was wrong.
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).
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).
Looking at some examples, all those \/ on every line are really ugly. Reminds one why the term `syntactic vinegar' was invented.
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."