[HN Gopher] Modeling Git Internals in Alloy, Part 2: Commits and...
___________________________________________________________________
Modeling Git Internals in Alloy, Part 2: Commits and Tags
Author : surprisetalk
Score : 111 points
Date : 2023-04-10 11:47 UTC (11 hours ago)
(HTM) web link (bytes.zone)
(TXT) w3m dump (bytes.zone)
| teeray wrote:
| How does Alloy compare to TLA+?
| hwayne wrote:
| Every time this comes up I promise myself I'll write a full
| post, and then I try to write a full post and give up 3000
| words later. Here's my usual, now-about-two-years-out-of-date-
| spiel:
|
| -------
|
| Alloy comes from the Z line of "systems are basically giant
| relational algebra problems", while TLA+ comes from the LTL
| line of "systems are basically giant temporal logic problems",
| which leads to a lot of fundamental differences between them.
| They also had different design philosophies: Jackson wanted a
| language that was easy to build tooling for, Lamport wanted a
| language that was easy to express complex logic in.
|
| One consequence of this is that Alloy is a much smaller
| language: you can fit the entire syntax on a single sheet. It's
| also much easier in TLA+ to write a spec that you can't model-
| check, while with Alloy you have to be actively trying. It's
| also impossible to write an unbound model in Alloy, so you're
| guaranteed that every spec is over a finite state space. Which
| gets rid of the common TLA+ runtime problem of "is this taking
| a long time because it's a big state space or because it's an
| infinite state space".
|
| Re tooling: Alloy converts to SAT, which makes model checking
| much, much faster. Specs that would take minutes to check in
| TLA+ take less than a second in Alloy. Being able to model-find
| as well as model-check is really nice, as is the ability to
| generate multiple counter/examples. The visualizer is really
| useful, too, especially for showing counterexamples to nontech
| folk. But the thing I honestly miss most when working in TLA+
| is the REPL. It's not the best REPL, but it's a hell of a lot
| better than no REPL.
|
| Okay, so drawbacks: Alloy6 added a notion of "time". This
| expands the space that Alloy can do, but the syntax is really
| footgun-heavy. If you forget to update a variable in TLA+, you
| get an error, if you forget to update in Alloy, it'll just
| assign whatever value it wants to that variable. I asked one of
| the developers and apparently it's not something they can
| easily address in the current semantics. Other problems are it
| can only check up to a given time-bound, which makes complex
| properties like liveness hard to check. The more "timelike" the
| problem gets, the worse Alloy becomes at handling it.
|
| Alloy also doesn't have composable collection types. You can
| model "a queue of messages", but you can't easily model "a
| queue of messages for each server". It's possible but you have
| to be clever, whereas in TLA+ it's straightforward.
|
| Less fundamental but still a big problem I keep having: no good
| iteration or recursion. Transitive closure is pretty nice but
| it's not powerful enough. For example: sig
| node {edge: set Node}
|
| Is N1 connected to N2? Easy, just do `N1 in N2^.edge`. How many
| nodes is the shortest path? That's much harder.
|
| Which one is more appropriate to use really depends on your
| problem. As a very, very, VERY rough rule of thumb: TLA+ is
| best you're most interested in the dynamics of a system: the
| algorithms, the concurrency, etc. Alloy is best when you're
| most interested in the statics of a system: the requirements,
| the data relationships, the ontology, etc. My standard demos
| for showcasing TLA+ are concurrent transfers and trading
| platforms, while my standard demos for Alloy are access
| policies and itemized billing. You can use each in the other's
| niche, too (see Zave's work on Chord), so it's a strict
| division.
| dgan wrote:
| Thanks it's really hard to navigate among different available
| tools as a n00b; so that clears it out!
| [deleted]
| rsrsrs86 wrote:
| Both can deal with time, but Alloy is a high level language to
| describe structures, their relationships, constraints and feels
| like writing SQL schemas and property tests. It is easy to use.
|
| With Alloy, you can very quickly iterate over software designs.
|
| TLA is more heavy weight and geared toward verifying concurrent
| systems, including algorithms and such. It is much harder to
| learn.
|
| With TLA, you can verify concurrent systems and algorithms.
| slaymaker1907 wrote:
| Allow is very different in that it approaches things by
| converting whatever you are trying to verify into first order
| logical formulae then trying to find some model which violates
| the formula. This is undecidable in the general case, but Alloy
| works around this by limiting the domain to some finite size
| (so considering all possible sets below some size) in which
| case the problem is merely NP-complete and easily translated
| into SAT.
|
| Because Alloy works off of first order logic, it's a lot more
| general than TLA+ but doesn't have temporal logic concepts like
| liveness as first class primitives. You can still model most of
| this stuff in Alloy, but I think Alloy is really best for when
| you want to verify something which doesn't have a good model
| checker available or in problem spaces which easily reduce to
| first order logic.
| hwayne wrote:
| > Because Alloy works off of first order logic, it's a lot
| more general than TLA+ but doesn't have temporal logic
| concepts like liveness as first class primitives.
|
| This is incorrect: TLA+ is also based off first-order logic
| constructs and can generally represent a much wider range of
| systems than Alloy can. The difference is that Alloy is more
| _tractable_ : what it can represent it can model check much,
| _much_ faster than TLA+.
| 0xDEF wrote:
| Last I checked Alloy was another wonderful specification language
| with bad or non-existent tooling.
| rsrsrs86 wrote:
| Curious, what do you think Alloy lacks in Tooling?
|
| I love the Alloy Analyzer. It's simple to use, you can
| visualize instances, it can point to UNSAT cores in the Code.
|
| (I wish it had a easy-to-use command-line or API so it would be
| easier to build a Web-based version of it.)
| hwayne wrote:
| Line numbers. Space-based indentation. Right-clicking. Find-
| replace.
|
| (Some of these might just be problems on Windows)
| picardo wrote:
| Agreed. Alloy IDE is pretty bad. I tried using external tools
| like [Sterling](https://sterling-js.github.io/), but they still
| rely on the IDE for some things.
| chrsig wrote:
| Does anyone know of a good hands on guide through learning how to
| use a model checker like alloy or tla+?
|
| I see lots of value in adopting them, but the dsl's that they use
| are inscrutable to me. I'm sure that after some hands-on time I'd
| understand them well enough, but having a hard time figuring out
| how to get that ball rolling.
| mdaniel wrote:
| Did you already watch the linked video
| (https://news.ycombinator.com/item?id=35512991) and go through
| Alloy's tutorial? https://alloytools.org/tutorials/online/
|
| Based on the approach taken by the presenter from the video,
| I'd guess the "hands on" you're looking for is to take some API
| that you serve to others, internally or externally, and start
| writing down things you believe are invariant about it. Inputs
| must have a length greater than 1? Well, do all downstream
| systems also honor that invariant?
| masklinn wrote:
| > But we also get some wilder instances. For example, it looks
| like our model allows trees to have commits as children: [...]
| Nope, doesn't work.
|
| That's not actually true: a submodule is a commit child of a
| tree.
|
| I'd assume the issue here is trying to add a child commit with
| mode 100644 instead of the submodule mode (160000), although tree
| modes are very much a wonky mess with inconsistent error
| reporting because there used to be more valid modes than there is
| now (100664), some of the error reporting is only under fsck, and
| influenced by traversal order, and bugs in the codebase made bad
| filemode detection plain not work until 2.38 (because file modes
| were checked post-normalisation).
|
| > Tags are like commits, but instead of pointing to a tree and
| parent they point to a commit
|
| Tags are not really like commits, and they can point to a blob, a
| tree, or an other tag just fine, which is why tags have a "type"
| header (the type / kind of the pointee).
| nextaccountic wrote:
| Yes, operationally tags are refs, just like branches
|
| (Even though the mental model people use for branches is
| different than tags
| https://blog.plover.com/prog/git/branches.html because when you
| make a commit when HEAD points to a branch, it updates the
| branch to point to the new commit, which doesn't happen with
| tags)
| ParetoOptimal wrote:
| I was exposed to alloy by this wonderful video:
|
| "Finding bugs without running or even looking at code" by Jay
| Parlar
|
| https://www.youtube.com/watch?v=FvNRlE4E9QQ
|
| I believe the general idea could be applicable in practice for
| core parts of most businesses software. So now I'm very
| interested in real world accounts of using alloy like this.
|
| Anyone have other posts like this one or experiences to share
| along these lines?
| rsrsrs86 wrote:
| I use Alloy extensively both to iterate designs very quickly
| and to communicate concepts to my team. My company is a SaaS
| for cap table management. I use it to formalize the core
| business logic as well as testing designs on non core features,
| like an account management system for example.
___________________________________________________________________
(page generated 2023-04-10 23:01 UTC)