K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

Just in case you didn't know about it, this paper is probably the right place to start for studying GC algorithms in a rewriting world:

FPCA 95: Morrisett, Felleisen and Harper
Abstract Models of Memory Management
http://www.ccs.neu.edu/racket/pubs/fpca95-mfh.ps.gz

Robby

On Mon, Jul 22, 2013 at 8:04 AM, Mark Hills <Mark.Hills AT cwi.nl> wrote:
>
> 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
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user