About the upcoming module system and Kôika's semantics

[mbty]

I'm interested in learning more about the upcoming module system. What are its main design objectives and how far along is it in its development? I also have one use case in mind that Kôika doesn't quite handle yet, and I wonder how the module system will impact it.

Here is a simplified, abstract example of it. Assume the following:

• In rule r1, there is a call to function f1 guarded by an if statement. The result of f1 is written to register g.
• In a separate rule, if g holds the value 1 at the beginning of the cycle, the external rule e is called.
• The only call to f1 that can possibly occur is the one in r1.

We want to prove the following property: "given schedule s and for all possible external semantics, whenever a call to f1 returns 1, e is called during the next cycle". This is complicated as of today, as all available semantics are register-centric, yet registers do not make an appearance here. More precisely, external calls are not considered for the reasons you detailed in issue #2 and both "TypedSemantics" and "CompactSemantics" erase the causality information that could be used to prove "when x is true, f1 is called and returns 1 and 1 is stored in g". It is of course possible to extract x, that is, the conditions under which f1 is called (remember that it is guarded by an if) and returns 1 (depends on the definition of r1), however in proving that when these are verified, 1 is stored in g, the link to the call to f1 is lost.

A more concrete example is as follows.

The rv example defines an isLegalInstruction function that is used to check whether a given word corresponds to an instruction according to the RISC-V specification. Currently, when an instruction fetched from memory turns out to be invalid, the program counter is set to zero, and the execution continues. If we wanted the processor to shutdown on an invalid instruction instead, we would have to modify RVCore to some extent. As the notion of shutdown is external to Kôika, we would have to rely on an external call to handle it (in fact ext_finish is already available).

We may be interested in proving the following property: "On the first cycle following one on which an invalid instruction was decoded (that is, one on which isLegalInstruction returned false), only one external call is issued. This call should be a call to the shutdown external rule. No other external calls can happen from this point on.".

I understand that the module system will probably have an impact on how external rules (including both those from other Kôika modules and "real" external calls such as ext_finish) are handled, with consequences on the semantics. Will the notion of calls to external rules indeed appear in the semantics? That should solve part of my problem. I guess it might not be the case for calls to rules of Kôika modules as those could be inlined as far as the logs go.

However, the more general problem of the lack of traceability of the causes of the actions tracked in the logs will likely persist as it is not really related to the notion of module as well as somewhat niche. The most obvious solution to this problem would be to develop yet another semantics with more detailed trace information and a proof of equivalence to the other ones in the situations they both cover. I guess that this is the route I will have to follow for the property I want to prove. Does this sound like the way to go or is there something simpler (maybe simply waiting for the module system is)?

[threonorm]

Hi,

The original intention was for external function to only be used for purely combinational functions. In that scenario registering calls to external function was not very relevant as external function were intended to be "generative", in the sense that two calls to the same external function were intended to generate 2 different circuits. This way no worries about sharing resources there.

In practice we used external function outside of this scope because this was quite convenient at times, so it may be reasonable to look at using them for your usecase, if you have low expectations and tolerate some hacks.

For your problem, @stellamplau had similar problems in her project to be able to model memory and various external modules (SRAMs and not just registers).

The way we went about it was modeling the process, it was a bit hacky, here is how it would work for your use case (stella feel free to correct me if I misremember):

• enrich the semantics to say that the state of the machine is (koikastate * bool), where the bool is the external state saying if the machine is up or not
• Define a new "cycle_with_external_world". Which composes in gallina the interp koika with a small functions that looks into the new value for the shutdown register, and if there is a request to shutdown in the koika shutdown register, raise the external gallina boolean to true.
• If the external boolean is high, don't do the interp koika

In that way you could decide to keep track of a trace of more than just a boolean, you can make arbitrary observation, and you can gallina proof about the whole system. Though you don't get good guarantees from compiler to verilog, as this machinery is invisible to it. To make the machine actually shutdown on FPGA, you would likely still need some call to an external function that would do nothing in the semantics but that would be the one doing the shutting down in the real circuit.

For your specific need of shutting down the machine, I think what I would do in your position (given what I understood) would be slightly different.
I would simply add a (! shutdown) guard to every single rules of my design.

Then I would prove that when shutdown is high, the state stays unchanged, and decide that this is what "shutdown" means. If my machine is part of a bigger trace generating system, this would be enough to show that once shutdown my processor does not emit anything, so observationally it would be indistinguishable from "shutdown". Does that make sense?

(Note: We use to have yet another construct, that was more like external rules, but we don't use it much, at least I have not used it in many months).

About the module system

In the module system each module as submodules, which have methods. And the semantics tracks the use of the methods as they track the use of read and write of registers. So in that system, you could prove that the submodule shutdown method is called exactly when it should be.

Though, one intention of the module system is to have a tree-like hierarchy (important for compilation), so to be able to have a submodule that shutdown the whole machine will be tricky even in that setup.

Because the modular compilation is tricky and fairly distinct from the current compilation strategy, the development is separated from koika (its currently a standalone project that uses a non-proven compiler written in Racket), the path to put that work in koika is not clear yet.