K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

Hi,

I'm watching the email thread and am interested in the topic.

I have two semantics written in K, a simulation relation from one to the other, and a handwritten simulation proof. It would be great to have my work checked by a tool.  That is why I am interested in your conversation.

As you take the conversation private (via skype), if you can also leave some info / breadcrumbs in public domain (like this email thread), that would be great!

Thanks!!

Daniel

On Sep 15, 2017, at 3:37 AM, Park, Daejun <dpark69 AT illinois.edu> wrote:

Hi Francesco,

That sounds very interesting, especially it tries to solve real problems! I'll be more than happy to talk more about it.

Is KEQ already available by any chance ?

Yes, but you will need my help to get started, since it is not yet user-friendly and has no document yet. But, you can take a look at an example to get the feel of it:

https://github.com/kframework/k/blob/keq-llvm/k-distribution/tests/equiv/test2/tests/while_spec.k

In the example, each 'rule' specifies each pair of the source and target programs (denoted by <L1> and <L2> respectively) and KEQ will automatically verify their equivalence given such a pair. We have more examples (loop code motion, constant propagation, x86 instruction selection, etc), but they haven't been published yet. (Yes, it is one of the latest work in our group!)

KEQ takes as inputs semantics of the source and the target languages, and a specification (called synchronization points) for each source/target programs, such as the 'rule' pair in the above example. Since we have the C semantics but not others (ORC, Matlab, R, etc.), you may need to specify the semantics of those languages to use KEQ.

We can set up a Skype/Hangout meeting to talk more if you want. Or, if you can provide a sample pair of the source and target programs that you mentioned, I can show you how to use KEQ to verify them.

Best,

Daejun

On Sep 11, 2017, at 3:29 AM, Bongiovanni Francesco A. <bongiovanni AT gmail.com> wrote:

Hello,

@ Everett : Thank you for your clarifications and pointers ! I will have a good look at CTL for expressing optimizations. I really look forward to the K mathematical definitions, hopefully it will trigger many interesting implementations.

@ Daejun : Thank you a lot for your input ! Is KEQ already available by any chance ?

The main reason I am in source-to-source translation using K is the following:

Part of my current job is split between CS research and the management/advance support of our HPC; in the HPC world, there is a ton of code which has to be ported to either more parallel friendly PLs (or the use of specific libraries). Most of the time, when I am doing that manually, requires not to break the original meaning of the software. What I see around me is that many of my colleagues (who are not CS researchers/specialists) are writing a lot of their algorithms in either Matlab, R, Python, IDL,... and even if these languages are great at prototyping, from a performance point of view, its awful. So ideally I prefer spending my time in writing tools to automate the rewriting process but with a certain confidence level obviously. I do believe in Prof. Rosu's approach, a PL should be rooted in precise semantics, and the derivation of tools from those precise semantics.

In general, I am interesting in lowering high level specifications to low level executable code. There are very interesting works around this from people in the Coq community (Bedrock, Fiat, ...). It would be interesting to see such kind of initiative in the K community.

@ both of you : thanks for your good work around K ! keep up the good work !

On 9 September 2017 at 01:25, Park, Daejun <dpark69 AT illinois.edu> wrote:

Hi Francesco,

> Given any two K formal semantics, let's say, C and ORC, do you think it is
> possible (and feasible) to create a K-based source-to-source translator that
> would translate a C program into an ORC program while retaining the semantics
> of the original C program ?


It depends.

In general there are two approaches: "verifying" the translation itself vs "validating" each of the translation instances. Note that I intentionally differentiate two terminologies: "verification" vs "validation".

We have a tool, called KEQ (which I'm working on), which is the program equivalence checker that are robust (i.e., general enough) for the "validation" purpose.

For some simple translations, you can still use KEQ for the "verification" purpose as well. By "simple", I mean the local translation rules such as the peep-hole optimizations.

We can talk more if you can share more details about your need. For example, what kinds of translations (or optimizations) you have in mind?

Best,
Daejun