k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] Source-to-source transformations / rule-based optimizations

From: "Park, Daejun" <dpark69 AT illinois.edu>
To: "bongiovanni AT gmail.com" <bongiovanni AT gmail.com>
Cc: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: Re: [[K-user] ] Source-to-source transformations / rule-based optimizations
Date: Fri, 8 Sep 2017 23:25:22 +0000
Accept-language: en-US
Authentication-results: illinois.edu; spf=pass smtp.mailfrom=dpark69 AT illinois.edu

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

[[K-user] ] Source-to-source transformations / rule-based optimizations, bongiovanni, 09/07/2017
- Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Everett Hildenbrandt, 09/08/2017
- Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Park, Daejun, 09/08/2017
  - Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Bongiovanni Francesco A., 09/11/2017
    - Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Park, Daejun, 09/14/2017
      - Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Daniel Schnetzer Fava, 09/15/2017