Choose and TLC

[fl]

Hi all,

 

"Choose x \in A : P" is a nice construct that allows to express ideas succinctly but

TLC evaluates it that way: it generates all the elements in A and then filter them using P.

If A is large, an exception is thrown.

 

A better way to evaluate the construct would be to generate an element of A, check that P is true,

if yes stop the algorithm in the other case continue. Obviously we can get too long a loop in that

case but in the better case we can have the opportunity to find the right element in a decent

time interval which cannot happen with the current algorithm. (Obviously if the loop is too

long we need a way to stop it.)

 

Generating one element at a time and then visiting it, is

the basic philosophy to evaluate combinatorial objects such as all trees or all permutations favored

by Knuth in TAOCP 4A.

 

--

FL

[Markus Alexander Kuppe]

Hi Frederic,

I added your idea to the Codeplex issue tracker [1] to look into it
later. I personally don't have the necessary bandwidth in the
foreseeable future though.

Thanks
Markus

[1] https://tlaplus.codeplex.com/workitem/24

[fl]

 

 

Hi Markus,

 

 

I added your idea to the Codeplex issue tracker [1] to look into it
later.

 

It is kind of you.

 

 

I personally don't have the necessary bandwidth in the
foreseeable future though.

 

OK. 

 

--

FL

[Leslie Lamport]

For the common case, in which there is a single element in the set satisfying the CHOOSE, this change would decrease the expected execution time of CHOOSE by a factor of two.  However, if you think about how TLC is probably written, it would require a separate version of the code to evaluate a set-valued expression for use in CHOOSE.  Moreover, this is one of any number of optimizations that one can think of.  For example, evaluating the common expression S = {} is probably now done by computing the value of  S  and comparing it to {}.  We need more than anecdotes to determine what optimizations are worth making.  In particular, changes to the costs of various parts of the computation have made expression evaluation an ever smaller part of the execution time of a TLC execution.  I believe that the biggest gains per programming hour are now obtainable by optimizing parallel execution and maintenance of the fingerprint graph.

Leslie 

[fl]

 

  We need more than anecdotes to determine what optimizations are worth making. 

It is not a question of optimization. I thought of cases where A is not a singleton.

 

In particular, changes to the costs of various parts of the computation have made expression evaluation an ever smaller part of the execution time of a TLC execution.  I believe that the biggest gains per programming hour are now obtainable by optimizing parallel execution and maintenance of the fingerprint graph.

I just wonder how many programmers have computers with parallel microprocessors at their fingertips :-) But I can understand that that aspect

can passionate an expert of parralel programming.

-- 

FL

 

[fl]

 an expert of parralel programming.

parallel programming.

 

-- 

FL

[Markus Alexander Kuppe]

On 02.02.2016 19:15, Leslie Lamport wrote:
> I believe that the biggest gains per programming hour are now obtainable
> by optimizing parallel execution and maintenance of the fingerprint graph.

I would add a third area to the list of improvements that have a good
return on invest. A profiler reveals a clear performance bottleneck
which affects the majority of models.

Cheers
Markus

[Leslie Lamport]

I haven't shopped for a computer recently, but I expect it's hard to find one with a processor chip that doesn't have at least 4 cores.  In a few years it will be hard to find one with fewer than 16 cores.  Every programmer in industry who is building the kind of large distributed system that requires TLA+ specifications should have access to a server farm with dozens or even hundreds of machines--e.g., by buying time on Azure or Amazon's cloud.  I want TLA+ to be useful for people who don't have much computing power--in part, because I want TLA+ to be taught at universities.  But ultimately, TLA+ will be successful only if it's used in industry.

I should also have mentioned that I believe that the most important area of TLC evaluation that needs improvement is its error reporting.  Speeding up evaluation saves computer time.  Speeding up finding the cause of an error saves human time.

[fl]

> Every programmer in industry who is building the kind of large distributed system that
> requires TLA+ specifications should have access to a server farm with dozens or even hundreds
> of machines--e.g., by buying time on Azure or Amazon's cloud. 

Sometimes I realize I'm far behind the reality already underway in the Silicon Valley :-)

(OK Amazon is in Seattle. And Seattle is not in the Silicon Valley but it is the idea.)

--
FL