K-user mailing list

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

The paper I mentioned uses a mark and sweep algorithm, but still a fairly 
basic one -- looking at more realistic garbage collection algorithms, like 
those used in actual languages, could be interesting. We were focused mainly 
on seeing if, even using a straight-forward algorithm, we could improve 
execution performance, but didn't look at the impact of this on our ability 
to analyze or verify programs.

----- Original Message -----
From: "Dwight Guth" 
<dguth2 AT illinois.edu>
To: "Mark Hills" 
<Mark.Hills AT cwi.nl>,
 "Emmanuel Castro" 
<emmanuel.castro AT laposte.net>
Cc: 
k-user AT cs.uiuc.edu
Sent: Monday, July 22, 2013 2:55:34 PM
Subject: RE: [K-user] Semantics of garbage collecting and store normalisation

You are also more than welcome to download the Python semantics I developed 
(found at http://code.google.com/p/k-python-semantics/) and examine the 
garbage collection algorithm it uses. It is fairly simplistic, being a very 
basic stop-the-world reference counting scheme, but it shows how you can 
recursively traverse the configuration to find all references to an object.


-------- Original message --------
From: Mark Hills 
<Mark.Hills AT cwi.nl>
Date: 07/22/2013 7:45 AM (GMT-06:00)
To: Emmanuel Castro 
<emmanuel.castro AT laposte.net>
Cc: 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] Semantics of garbage collecting and store normalisation


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
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user