[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC Nat and Integers...still using 32 bit?
I don't think "doubling the on-disk representation" of integers would be significant for most users, if any. Disk space and memory is very cheap. Additionally, the values have wrapper types anyway: https://github.com/tlaplus/tlaplus/blob/6479e53ae1e418a1bfe31677ad45012fe8ed7008/tlatools/org.lamport.tlatools/src/tlc2/value/impl/IntValue.java#L19 . This means (I think) that the value will be heap-allocated, and as such will have a 64 bit pointer attached to it for reference and deference. As such, I don't think the difference from "int" to "long" would be significant.
I'm skeptical of the claim that it would result in "slower performance". 64 bit CPUs should be able to handle longs at the same speed as ints, and I suspect that whatever performance "gains" you would get from using 32 bit int would be dwarfed several times over by the latency of fetching from the heap to unbox the value.
My goal was actually to use TLAPS, and I was just using TLC to sanity check my implementation of Collatz, because obviously a model checker can't check the entirety of naturals, though I think TLAPS doesn't have support for some of the operators I'd need for my ideas.
On Tuesday, July 29, 2025 at 12:40:47 PM UTC-4 Markus Kuppe wrote:
Generally, it's best to discuss TLC bugs and enhancement requests at github.com/tlaplus/tlaplus. That said:
TLC does work on 32-bit architectures. However, in that environment, you won’t be able to take advantage of the faster CAS-based fingerprint set implementation and will have to rely on the slower, platform-independent version instead.
As for switching TLC from 32-bit to 64-bit integers: I don’t see how this could be done without significant cost. At a minimum, it would double the on-disk representation of integers, unnecessarily increasing storage usage in most cases. This doesn't even account for the potential for subtle bugs introduced by changing from int to long. Java’s type system doesn’t make such transitions trivial in a complex codebase like TLC’s.
More fundamentally, I’d want to see a broader set of real-world specs and models that would benefit from 64-bit integers. For most existing TLC models, this change would result in slower performance with no practical gain. We would essentially be optimizing for an outlier. As Igor mentioned, these scenarios are better served by a tool like Apalache, which is designed for symbolic execution and unbounded arithmetic. TLAPS is another tool to mention here.
Markus
> On Jul 29, 2025, at 7:49 AM, Andrew Helwer <andrew...@xxxxxxxxx> wrote:
>
> Regarding 32- or 64- bit arithmetic, TLC already does not work on 32-bit architectures due to a 64-bit atomic compare-and-swap operation it does on the fingerprint set, which uses 64-bit hashes. So theoretically there shouldn’t be any performance hit to using longs for arithmetic instead of ints. It is possible it would cause the pending state set to take up more memory, though. I don’t know whether 32-bit integers are already aligned to a 64-bit boundary in Java datastructures, or what.
>
> BigInteger isn’t a good idea in my opinion because TLC models tend to use small numbers amidst combinatoric state explosion, so performance is very important.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/3578a141-6759-41e9-b45b-5b03d64ca517n%40googlegroups.com.