5 ms·
> you can already use a SAT solver Could you elaborate please? How would you approach this problem, using a SAT solver? All I know is that a SAT solver tells y
by ksclk 1y ago
> you can already use a SAT solver
Could you elaborate please? How would you approach this problem, using a SAT solver? All I know is that a SAT solver tells you whether a certain formula of ANDs and ORs is true. I don't know how it could be useful in this case.
- dragontamer 1y agoPretty much all instructions at the assembly level are sequences of AND/OR/XOR operations. SAT solvers can prove that some (shorter) sequences are equivalent to other (longer) sequences. But it takes a brute force search. IIRC, these super optimizing SAT solvers can see patterns and pick 'Multiply' instructions as part of their search. So it's more than traditional SAT. But it's still... At the end of the day.... A SAT equivalence problem.
- agent327 1y agoA short look at any compiled code on godbolt will very quickly inform you that pretty much all instructions at the assembly level are, in fact, NOT sequences of AND/OR/XOR operations.
- dragontamer 1y agoAll instructions are implemented with logic gates. In fact. All instructions today are likely NAND gates. Have you ever seen a WallaceTree multiplier? A good sequence that shows how XOR and AND gates can implement multiply. Now, if multiply + XOR gets the new function you want, it's likely better than whatever the original compiler output.
- saagarjha 1y agoComputers are not programmed on the level of logic gates. If you want to do that, design an FPGA.
- dragontamer 1y agoSuperoptimizers take this stuff into consideration. Which is what the parent post was talking about, the rare superoptimizer.
- agent327 1y agoThat was not the claim. The claim was that assembler was made up out of sequences of OR/AND/XOR, and that claim is demonstrably false.
- astrange 1y ago"Made up of" isn't helpful. All assembly languages are equivalent to a sequence of bit operations. (…if you ignore side effects and memory operations.) In fact there's several different single operations you can build them all out of: https://en.wikipedia.org/wiki/One-instruction_set_computer#Instruction_types https://en.wikipedia.org/wiki/One-instruction_set_computer#I... So you take your assembly instructions, write a sufficiently good model of assembly instructions<>bit operations, write a cost model (byte size of the assembly works as a cheap one), and then search for assembly instructions that perform the equivalent operation and minimize the cost model. Like here: https://theory.stanford.edu/~aiken/publications/papers/asplos06.pdf https://theory.stanford.edu/~aiken/publications/papers/asplo...
- viraptor 1y agoYou're missing forest for the trees and lacking information to discuss this really. Check out this paper and similar ones if you want to learn about this area: https://arxiv.org/pdf/1711.04422 https://arxiv.org/pdf/1711.04422
- dragontamer 1y agoWhat do you think implements assembly language? Answer: Verilog or VHDL. And these all synthesize down to AND/OR/XOR gates and eventually converted into NAND gates only. Every assembly language statement is either data movement, or logic, or some combination of the two. ------- We are talking about SAT solvers and superoptimizers. Are you at all familiar with this domain? Or have you even done a basic search on what the subject matter is?
- LtWorf 1y agoIf you want something optimised… "equivalent" isn't going to do it.
- viraptor 1y agoYou're missing the point. All instructions can be simplified to short integer operations, then all integer operations are just networks of gates, then all gates can be replaced with AND/OR/NOT, or even just NAND. That's why you can SAT solve program equivalence. See SMT2 programs using BV theory for example. Also of course all instructions are MOV anyway. https://github.com/xoreaxeaxeax/movfuscator https://github.com/xoreaxeaxeax/movfuscator
- agent327 1y agoI seem to remember that program equivalence is an NP-hard problem. I very much doubt that you can solve it by reducing it to logic gates.
- viraptor 1y agoNP-hard is just a complexity class, not a minimal threshold. SAT solving is kind of a guided optimistic bruteforcing. If the example is small enough, you can still solve it very quickly. Same as you can solve travelling salesman for a small number of cities. We solve small cases of NP-hard things all over the place.
- viraptor 1y ago(not to confirm it's an np-hard problem - it may not even be decidable generally, but in practice yes, you can check it that way and SMT2 theories provide the right ops)
- dragontamer 1y agoThat's why superoptimizers work on short sequences of code and take a long time doing so.
- valkon 1y ago[dead]
- dataangel 1y agoYou're a bit naive about the complexity. Commonly longer sequences are actually faster, not just because instructions vary in their speed, but also because the presence of earlier instructions that don't feed results into later instructions still affect their performance. Different instructions consume different CPU resources and can contend for them (e.g. the CPU can stall even though all the inputs needed for a calculation are ready just because you've done too many of that operation recently). And then keep in mind when I say "earlier instructions" I don't mean earlier in the textual list, I mean in the history of instructions actually executed; you can reach the same instruction arriving from many different paths!
- astrange 1y agoHmm, this usually doesn't come up simply because you're usually targeting multiple different CPU generations at once, and then the details cancel each other out. The most ffmpeg has had to do in this area is that some CPUs had very slow unaligned memory loads and some didn't.
- LtWorf 1y agoI see a guy who has never seen assembly explain assembly to people who have written assembly and written compilers and optimisations…
- peaboff 1y agoWhat you're saying is true. Yes you can grind away at generating sequences of instructions, SAT solve equivalence and benchmark, but of course, you would sooner see all black holes in the observable universe evaporate before you find an instruction sequence that is both correct AND 100x faster.