K-user mailing list

["Bongiovanni Francesco A." <bongiovanni AT gmail.com>]

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