Hi Jonas,
Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx> writes:
[...]
> I meant that we implemented an internal tool to transpile from C
> to PlusCal.
I'm curious about the design/architecture here - how did you manage the
logical mappings from C->PlusCal - did you have a third language to
specify the mappings, or did you use heuristics with inherent
assumptions ?
> It sounded like a great idea at the time. But then it quickly fell
> out of use.
This is something I'm keen to understand why - was this because
programmers focussed on the C code, and the transpiler+constraints
became a "testing problem" which ended up in bitrot ? Or is there
something related to the software methodology/development process ? Or
perhaps the percieved ROI of formal verification wasn't as much as
initially thought ? Something else ?
[...]
> For reuse, I think the main issue is that implementation code is
> always a source of truth - the truth of what's really going to be
> executed. If we want to have a second source of truth, it should
> be a different truth, such as "assumptions of the other parts of
> the system".
> Since you already have this source of truth, if you make a
> different implementation in another kernel, you can compare what
> the original driver was doing with what your new implementation is
> doing. There's no need to have yet another copy of what the
> driver might be doing.
I understand what you're saying, but there are a few points that I'm
probably not able to express clearly.
Just to set context, and not to state the obvious - as you likely
already know, Formal languages such as pluscal or promela have an
"execution model" that is different from a programming language - in
that, when one writes code in them, one's mental model needs to pay
attention to behaviour, whereas function becomes a more abstract
problem[...]. I wrote a very hand wavy description of
this in the context of spin:
https://mail-index.netbsd.org/tech-kern/2023/09/28/msg029203.html
So to return to your concern about code duplication, in the context of
codegen, one could make the same argument about compiled or transpiled
code - if it were manually transpiled. And yet we are comfortable as
programmers, assuming that the "higher level language" is the source of
truth, while happily stepping "down" to gcc __inline__ __asm__ {} when
needed. So, for eg: (and I believe there are tools out there that can
do this to some degree) - if the programming code could be
auto-generated/"compiled" from the formal specification, then this would
become directly analogous.
[...]
>> Can you give me an example of how this works/a pre-existing tool
>> that helps with this simplification ? I'm actually currently
>> looking at re-writing modex to do precisely this (but with the
>> translation end-point being something close to the original
>> model).
> I think any higher level language, including C, goes into this
> direction. Some are just a lot better at building abstractions and
> describing the code more model-like than
> tiniest-implementation-detail-like.
C is problematic because it doesn't for eg: define concurrency or
consistency models - in many cases, even the data types are not clearly
defined (eg: "integer" is machine word size dependant). So it's really
hard to specify something formal at the level of C that is not very
context (OS/CPU arch) specific.
> By executable comment I mean a comment that has a formal semantics
> that can be executed.
> Think more pre&post conditions + ghost code. E.g., for a tricky
> sort algorithm like timsort the comment might be something like
> var __ghost_array = copy(input_array);
> .... // complicated timsort code here
> insertion_sort(&__ghost_array); // timsort should give the same
> output as insertion stort, note that both are stable
> for (i in 0...array_len) { assert (sorted_array[i] ==
> __ghost_array[i]); }
> This is probably not going to help you find the well-known timsort
> bug, but it might be enough to find more trivial mistakes when
> rolling your own timsort. Anyways this is what I mean by
> executable comment - a more readable, maintainable implementation
> of the code that tells you what the code ought to be doing + some
> checks to say that they're really doing the same thing.
This looks closer to testing to me - the assertions for eg: seems to be
atemporal ie; only concerned about "immedate" values, unlike LTL which
can check behaviour across an "execution sequence" (in the set of all
possible execution sequences). So from an FV perspective, I would write
the assertion to look more like: "eventually is_sorted(array)", where
is_sorted() has magic to check to if the array elements are sorted in
whatever required order.