(I'm no expert but..) I recently got into Prolog, and Alloy sounds very similar. So I was asking "How is it different?" Strangely, in the FAQ, no mention of Prolog. I found just this:
>How does the Alloy Analyzer differ from theorem provers?
>The Alloy Analyzer's analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It's a "refuter" rather than a "prover".
(i.e. where Prolog would just write "no" if nothing found.) In the Alloy* paper also, no mention of Prolog. To find a counterexample, couldn't you set Prolog to find one?
Prolog is a general programming language with built-in backchaining semantics. It in general does not know how to solve constraints. Indeed if your clauses have loops Prolog will just run in circles until it is out of stack space. The following common rules for equivalence are good examples of valid logic statements that do not work with Prolog's naive execution strategy:
% Symmetry
f(A, B) :- f(B, A).
% Transitivity
f(A, C) :- f(A, B), f(B, C).
Indeed in general finding the symmetric/transitive closure of relations is a very hard problem. Constraint/SAT solvers use heuristics to solve problems like the above and can accept much more declarative specifications than Prolog.
You could try in Prolog. But the other difference is that prolog is. General purpose language (though used in a more specific set of situations). Alloy is not.
Also the search mechanisms are not the same. Prolog uses a backtracking, depth-first search behind the scenes. Alloy does not.
EDIT: I was out earlier and didn't want to make a claim I couldn't verify/backup. Alloy uses a SAT solver behind the scenes to find solutions.
Alloy is a specification language. To verify the specification, the alloy analyser (a model checker) has to artificially create some number of instances and simulate it.
Prolog is an executable language. You, the user, give it a database, and it searches for solutions that satisfies constraints. It doesn't create the basic facts on its own.
There exists a compiler from imperative alloy to prolog to make this transition.
Hmm well, not all Prolog uses fit the 'give it a database' model..(In fact I can't think of any Prolog programs I've seen that do fit it) e.g. I was tried the the finite domain solver in Gnu Prolog[0] recently, I wanted arrangements of about 15 shapes that obeyed certain constraints, the program was 6 very short lines! I didn't tell it anything except the constraints.
But yeah, alloy and alloy* sound fascinating, I must investigate further, thank you.
You are right. Constraint solving in general is a specific area that does not require a knowledge base; instead it is a search for a solution from the specified domain that fits all the specified constraints. Here there is considerable overlap between prolog, alloy and z3.
However, most general prolog programming has the same requirements placed on other executable languages, to transform, store and communicate data. Alloy is not the tool for this aspect.
Prolog is Turing-complete, you can have non-terminating programs in it (and thus there are problems that can be expressed in Prolog that you can never get an answer to), does the same hold true for Alloy? If not I think that it would make more sense to compare Datalog (which I think forces all of its programs to provably terminate) with Alloy rather than Prolog with Alloy.
Too bad, A72 is the sort of thing found in $49 SBC's these days. For the price, it would have been nice to see at least A73, but at least its not an A53.
True, most server ARM processors that come to mind are custom (or at least semi-custom): Ampere, Centriq, ThunderX2. Trying to map them to A72/73/75/76 is perhaps short sighted since those are primarily smartphone cores - we'll have to wait and see how they perform in real world tests.
Probably should have done a lscpu instead. On recent arm distro's lscpu knows how to decode the part/variant/etc and it also pays attention to the cache and numa topology.
It’s certainly possible, though it comes with a different set of challenges to software verification. Here’s a recent paper in this direction, proving the correctness of a RISC-V CPU: http://plv.csail.mit.edu/kami/papers/icfp17.pdf
Polyhedral optimisation is cool (Facebook has been using it to great effect for ML kernels recently [1]), but it’s not the end of the story. It’s complementary to this paper, which seems to be about learning an effective and transferrable cost model to guide the optimisation process (you could use that learned cost model in a polyhedral optimiser).
Running on a Zedboard is quite well documented; only took me a couple of hours to do it from scratch following their instructions: https://github.com/ucb-bar/fpga-zynq
