K-user mailing list

[Mark Hills <Mark.Hills AT cwi.nl>]

Hi Manu,

We actually looked at garbage collection in an OO language in this paper:

http://fsl.cs.uiuc.edu/index.php/Memory_Representations_in_Rewriting_Logic_Semantics_Definitions

Note that this wasn't using the K framework, but instead used a K style of 
definition with rewriting logic semantics and Maude.

I do think that normalizing the store would be an interesting topic to look 
at. It definitely isn't trivial -- there has been some work in K on creating 
an abstraction of memory usage for programs that cycle (I believe the proper 
reference is here: 
http://link.springer.com/chapter/10.1007%2F978-3-642-37635-1_4), and I'm sure 
there are many other opportunities to apply techniques from areas like 
symmetric reduction to K specifications. If there is other work on this that 
I haven't mentioned, hopefully someone else on the list will jump in :)

Cheers,

Mark

----- Original Message -----
From: "Emmanuel Castro" 
<emmanuel.castro AT laposte.net>
To: 
k-user AT cs.uiuc.edu
Sent: Monday, July 22, 2013 12:05:50 PM
Subject: [K-user] Semantics of garbage collecting and store normalisation

Does someone has ever worked on garbage collection in K? 
I would like to mesure the memory consumption of some programs, and thus I 
want to remove the unused elements from the store. 

More generaly, I am interested in normalising the store. During a 
non-deterministic krun, I often end up with syntactically different, yet 
semantically equivalent configurations. 

<env> a |-> #symInt(1) b |-> #symInt(2)</env> 
<store> #symInt(1) |-> "aa" #symInt(2) |-> "bb" </store> 
vs. 
<env> a |-> #symInt(2) b |-> #symInt(1)</env> 
<store> #symInt(1) |-> "bb" #symInt(2) |-> "aa" </store> 

Is there well known techiques of normalisation? 

Merci d'avance 

Manu 

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user