Maude-help mailing list

[Phillip Schanely <pschanely AT gmail.com>]

Francesco, Steven,
Thank you for your (detailed!) thoughts. Tending to a mailing list is
a lot of work, even if you enjoy the topic! At any rate, this has been
really helpful for me.

Steven, I'm really glad that things are happening with Maude, even if
rewriting isn't fashionable at the moment.  Unification modulo
associativity sounds particularly exciting!  And thanks for the
practical pointers about degenerate data and rules versus equations.
Those are exactly the sorts of conclusions that are hard to reach when
you're teaching yourself.

Francesco, so many great leads!  The HOL work in Maude is interesting;
honestly, even just reading real Maude modules is helpful to me (I am
just getting the hang of parameterized modules).  Your message made me
realize that I need to motivate this work more: in summary, I am
interested in optimization that is high level and very late. I'm
interested in something that might, for instance, take a unix command
line like "cat foo.txt | sort | tail -1" and (with suitable functional
definitions of all those operators) convert the full sort into a
linear scan.  For the most part today I can do that with plain
rewriting in Maude, but in order to do that, I had to put a lot of
thought into code movement between higher order functions.
I've just skimmed the paper you mentioned about parallelizing by
symbolic execution; it is very much the sort of thing I need to find
more of.  I'll dig into the CGO proceedings; sadly, I was unaware of
that conference (I've been out of academia for too long!).  Finally,
yes, the K framework (and of course llvm) looks like something I need
to play with as well.  Thank you!

Oh and let me know if you guys find yourself in New York at some
point; I think there are a few meetups here that would love to have
someone come and give an introduction about rewriting systems, Maude,
semantics, or verification.

Thanks again!
  Phil


On Wed, Apr 27, 2016 at 2:19 AM, Francesoc Bongiovanni
<bongiovanni AT gmail.com>
 wrote:
> Hi Phil,
>
> I also play with Maude around higher order functions, for other purposes 
> than
> compiler optimization.
>
> First of, here is a link you might have a look at :
> https://github.com/ephoning/maude/blob/master/higher-order
>
> have a look at the ho-func3.fm and ho-func-test3.fm files, I based with
> current work on these implementations of map/reduce HO functions, they are
> quite neat.
>
> I had a look at your blog post, I think I got more or less what you are 
> trying
> to achieve but something struck me a bit. Generally, when one uses the Map/
> Reduce programming model they tend not to put map inside a reduce and keep 
> the
> two `stages` clearly separated anyway, but a very good `optimization` for 
> map/
> reduce programs actually is to lift up functions in the reduce in the mapper
> (that's what people did inside Apache Spark optimizations) and there is 
> also a
> nice research paper you might find interesting from SOSP'15 entitled
> `Parallelizing user-defined aggregations using symbolic execution` from
> Raychev et al. which promotes a new way to deal with loop-carried 
> dependencies
> using symbolic execution. I am pretty sure you will find them interesting :)
>
> Have a  look at proceeding of the CGO conference which you probably know 
> (The
> International Symposium on Code Generation and Optimization) there are a lot
> of nice papers around what you want to do.
>
> Something very related to maude is the K-framework (www.k-framework.org).
> Prof. Grigore Rosu and  University of Illinois and his group along with 
> people
> from Romania did some impressing work around term rewriting.  Think of if 
> as a
> very nice tool to encode programming language semantics and develop formal-
> based tools for creating languages, reasoning about programs, and so 
> on...the
> initial K tool had Maude as a back end (they are switching as we speak to 
> get
> more performance) and they have formalized the semantics of Java 1.4, almost
> all C, verilog, scheme,...and LLVM IR (which may be of interest to you) .
>
> Cheers,
>
> - Francesco
>
>