K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Francesco,

Source to source translation might be difficult given nothing but the 
semantics, but fortunately you may not have to do that.
We have a program equivalence checker which can check the equivalence of two 
programs (even if they are written in different languages).
You have to provide the bisimulation relation between the two languages, but 
after that it should go through.
Daejun perhaps you can say some more about this?

Using this approach, you would provide an external translator from C to ORC 
and then just validate each instance of translation.
This may not be as desirable as a full-blown correct-by-construction 
translation, but is probably also much cheaper.

In terms of source-level optimizations of programming languages, I did begin 
a project my first year here using CTL formula to specify optimizations.
I didn't make it much further than specifying the semantics of CTL, as I was 
pretty inexperienced at the time.
Many compiler transformations can be expressed using CTL formulae, see 
[Specifying and Executing Optimization for Parallel 
Programs](http://egunter.cs.illinois.edu/papers/GRAPHITE2014.pdf) and other 
work by William Mansky/Dennis Griffith/Elsa Gunter.
In that work, they use normal CTL for the side-conditions of the 
transformations, and build the transformations out of basic graph 
manipulations.
In K, it would be natural to use Matching Logic patterns as the atomic 
predicates underneath the CTL formula.

This would be a little different than the algorithmic approach taken in the 
paper you sent.
The main benefit of using CTL formulae as side conditions is that proving the 
correctness of the transformation becomes much simpler, as you can express 
the correctness of a compiler optimization directly as a CTL formula.

We are working on documenting how K works mathematically so that others can 
produce their own implementations and understand our better.
Perhaps Xiaohong can say some words about progress on that.

Regarding documentation on the internals of K the implementation, that is 
unfortunately sorely lacking.
It is on our to-do list and we are slowly putting it together, but there is 
only so much time to allocate to such things :/

Let us know if you have more questions,
Everett H.

On Thu, Sep 07, 2017 at 09:09:40AM -0500, 
bongiovanni AT gmail.com
 wrote:
> Hello,
> 
> I would like to have a K expert opinion about a specific usage I have in
> mind.
> 
> I've been toying with K yet I wonder this thing :
> 
> 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 ?
> 
> Did some folks at UUIC work on that by any chances ? is there any interests 
> in
> doing such a thing ?
> 
> I am also interested in rule-based optimizations with K (Seokje Seo did a 
> nice
> Msc thesis about that :
> https://www.ideals.illinois.edu/bitstream/handle/2142/88962/SEO-THESIS-2015.pdf?sequence=1),
> I tried to replicated his stuff with no success..., is there any proper
> documentation regarding the internals of K ?
> 
> Thanks in advance !
> 
> Cheers !
> 
> - Francesco