Controlix takes a hit!

I was browsing through some compiler-related stuff on Wikipedia yesterday, and I came across this:

https://en.wikipedia.org/wiki/ROSE_(compiler_framework)

This is a very well-written compiler-to-compiler framework which supports several "meta-compiler" techniques, the important one of which here is this:

https://en.wikipedia.org/wiki/Automatic_parallelization

Using auto-parallelization allows for extracting fine-grained multithreading out of standard code. The package in Rose which does this produced code which can be fed into OpenMP, and it will even suggest fixes for existing manually-parallelized OpenMP code! This means that you can mix code with explicit spinlocks and regular code, which in turn means that spinlocked code (such as operating system code) can be generated for existing operating systems (e.g. Linux) without having to rewrite much if any of the existing code (aside from having to use OpenMP locks specifically).

What does this mean for Controlix? Well, much of the reason for using controlix was to improve performance, which is not (at least in principle) gone. Much of the rest of the justification for using controlix was to lock out with proofs, but I was counting on massive performance improvements to "sell" Controlix to an audience which probably isn't going to be using langauges like Verilog or SpecC to write pure software anytime soon. Remember, folks, all computers are based on turing machines, and, with the exception of wierd analog mixed-signal stuff which is an edge case, they are either faster or slower than other computers. Period. Now that there is a decent way to produce totally-optimal multithreading without forcing people to switch languages, Controlix-loses a major selling point.

The main selling point of Controlix, IMHO, is of course the possibility of fine-grained provability of behavior via testbenching, which is (again IMHO) a public safety issue and worthy of promotion, so Controlix is far from dead. You simply cannot do that type of thing on non-RTL-type languages, period. However, much of the existing bug set in the field revelves around race conditions, which automatic parallelization techniques will pretty much wipe out. So, I congradulate the folks at LLNL (the authors of Rose), and hopefully I will someday be able to locate a way to proof-check standard C code (maybe Z3: https://github.com/Z3Prover/z3/wiki#background), which would pretty much obsolete Controlix. Until then, onward!