I have to say, I need to try to publish my work more often. (For other than
the obvious reason that I need to publish work, period.)
It really forces you to make everything concrete. To the max.
Almost as much as actually implementing it would.
the informal ramblings of a formal language researcher
Friday, April 29, 2005
Tuesday, April 19, 2005
System F and semi-unification
This is somewhat of a note to myself to revist the responses posted.
I'm not 100% percent sure the original author (Mike) really had a grasp on what he was saying. On the one hand, he wanted to get an intuition as to which programs would be problematic to infer types for. But then he started talking about reducing inference for those problems to semi-unification; that's not the right idea! The idea is that you take a bog-standard undecidable problem (e.g. the halting problem), reduce that to semi-unification, and then reduce the reduction to a sample term in System F.
Of course, this would probably yield a term so complex that it would boggle the mind, and not provide the intuition that he was hoping for.
If, on the other hand, he was just interested in the idea of using a (partial) semi-unifier to (partially) perform type inference for System F, then that's a different story. Hard to tell. But lots of interesting points and links in the responses.
I'm not 100% percent sure the original author (Mike) really had a grasp on what he was saying. On the one hand, he wanted to get an intuition as to which programs would be problematic to infer types for. But then he started talking about reducing inference for those problems to semi-unification; that's not the right idea! The idea is that you take a bog-standard undecidable problem (e.g. the halting problem), reduce that to semi-unification, and then reduce the reduction to a sample term in System F.
Of course, this would probably yield a term so complex that it would boggle the mind, and not provide the intuition that he was hoping for.
If, on the other hand, he was just interested in the idea of using a (partial) semi-unifier to (partially) perform type inference for System F, then that's a different story. Hard to tell. But lots of interesting points and links in the responses.
subtextual response
I've been looking at Jonathan Edwards' experimental programming
environment/language, Subtextual
I am semi-underwhelmed. But there are some interesting connections with spreadsheet programming here.
I later read this post from the related Alarming Development blog, and there was one thing there that irk'ed me: the idea that we should embraced copy-and-paste programming.
cut-and-paste programming, I have learned to accept. That's when, if you are tempted to copy-and-paste a snippet of code, you instead cut it out entirely, and then turn it into a seperate subroutine/superclass/unit/module. Then you parameterize accordingly (and of course you are expected to add documentation about the mental model you have in your head about what this piece of code does).
But copy-and-paste is very dangerous. And in fact, in Subtextual, it seems like Edwards has embraced a sort of hybrid between cut and copy, because when you copy subtrees, you don't get a fresh copy immediately; instead you get a tree that is linked back to the original tree, and changes to either will propogate to both. You have a seperate operation, "introduce variant", to actually do the copying in place.
environment/language, Subtextual
I am semi-underwhelmed. But there are some interesting connections with spreadsheet programming here.
I later read this post from the related Alarming Development blog, and there was one thing there that irk'ed me: the idea that we should embraced copy-and-paste programming.
cut-and-paste programming, I have learned to accept. That's when, if you are tempted to copy-and-paste a snippet of code, you instead cut it out entirely, and then turn it into a seperate subroutine/superclass/unit/module. Then you parameterize accordingly (and of course you are expected to add documentation about the mental model you have in your head about what this piece of code does).
But copy-and-paste is very dangerous. And in fact, in Subtextual, it seems like Edwards has embraced a sort of hybrid between cut and copy, because when you copy subtrees, you don't get a fresh copy immediately; instead you get a tree that is linked back to the original tree, and changes to either will propogate to both. You have a seperate operation, "introduce variant", to actually do the copying in place.
Tuesday, April 12, 2005
mailman, postfix, and pain
Was up late last night trying to set up a mailman-based mailing list to demonstrate such things to my cousin.
I made much use of this page to figure out how to get the whole thing going. But when I went to bed, the damn thing still wasn't working.
Eventually I figured out that I never actually started the mailman daemon that is in charge of processing information as it comes in. I just figured that apache and postfix would know that they needed to call out to these command line procedures when they got certain inputs (e.g. mail to a particular address). Silly me.
So I was dumped into the sewer of systems administration once again. But I've pulled myself out now; I'm so happy I'm a PL researcher.
I made much use of this page to figure out how to get the whole thing going. But when I went to bed, the damn thing still wasn't working.
Eventually I figured out that I never actually started the mailman daemon that is in charge of processing information as it comes in. I just figured that apache and postfix would know that they needed to call out to these command line procedures when they got certain inputs (e.g. mail to a particular address). Silly me.
So I was dumped into the sewer of systems administration once again. But I've pulled myself out now; I'm so happy I'm a PL researcher.
Monday, April 11, 2005
Observing Finalizers and References on the JVM
As a followup to clarify my previous comment on this post (since Dave and I discussed this question personally):
Here is an experimental revision of the code that Dave posted; it is meant to demonstrate a number of things. The most important are:
I had to backport the code to JDK 1.4 since that's all I have on my poor little Mac OS X box. Sorry. I tried to make the backport clean by using trampoline instantiation of the generic collections rather than cluttering up the code with casts everywhere.
Sample command line invocations of this class:
(Note that due to the braindead way I'm doing argument parsing, the order of the options above is VERY significant).
Here is an experimental revision of the code that Dave posted; it is meant to demonstrate a number of things. The most important are:
- If you want to really observe a space leak, it is helpful to actually use objects which are large (
new int[X]
is your friend here). - If you want to really observe a space leak, it (unfortunately) seems like you may have to employ the (non-standard)
-Xms
and-Xmx
options to the JVM. - There are more reliable/sensible alternatives for monitoring whether an object has been collected than attempting to maintain a hashtable of object identifiers. Namely, use of classes in
java.lang.ref.*
.- Having said this, I admit that I do not fully understand the semantics of weak references, because I was not able to naively replace all of Dave's uses of
kill(int)
with mykillAlt(int)
procedure.
- Having said this, I admit that I do not fully understand the semantics of weak references, because I was not able to naively replace all of Dave's uses of
- Finalizers really are run only once. However, that doesn't always mean that you can't collect an object just because the call to its finalizer makes it live again.
I had to backport the code to JDK 1.4 since that's all I have on my poor little Mac OS X box. Sorry. I tried to make the backport clean by using trampoline instantiation of the generic collections rather than cluttering up the code with casts everywhere.
Sample command line invocations of this class:
% java -Xmx1mb -Xms1mb Immortal -dummysize 100000 -num 10
% java -Xmx1mb -Xms1mb Immortal -dummysize 100000 -blowup 10
(Note that due to the braindead way I'm doing argument parsing, the order of the options above is VERY significant).
import java.util.Hashtable;
import java.util.Vector;
import java.lang.ref.Reference;
import java.lang.ref.WeakReference;
import java.lang.ref.ReferenceQueue;
public class Immortal {
static class HashtableFromIntegerToInteger {
Hashtable me = new Hashtable();
public int get(int k) { return ((Integer)me.get(new Integer(k))).intValue(); }
public void put(int k, int v) { me.put(new Integer(k), new Integer(v)); }
public void remove(int k) { me.remove(new Integer(k)); }
}
static class HashtableFromIntegerToImmortal {
Hashtable me = new Hashtable();
public Immortal get(int k) { return ((Immortal)me.get(new Integer(k))); }
public void put(int k, Immortal v) { me.put(new Integer(k), v); }
public void remove(int k) { me.remove(new Integer(k)); }
}
static class HashtableFromIntegerToRef {
Hashtable me = new Hashtable();
public Reference get(int k) { return ((Reference)me.get(new Integer(k))); }
public void put(int k, Reference v) { me.put(new Integer(k), v); }
public void remove(int k) { me.remove(new Integer(k)); }
}
/** tracks the number of times each finalizer is run */
// private static HashtablefinalizeCounts = new Hashtable ();
private static HashtableFromIntegerToInteger finalizeCounts = new HashtableFromIntegerToInteger();
/** used to control object lifetimes */
private static HashtableFromIntegerToImmortal pointers = new HashtableFromIntegerToImmortal();
private static HashtableFromIntegerToRef phantoms = new HashtableFromIntegerToRef();
private static ReferenceQueue refqueue = new ReferenceQueue();
private static boolean nomesg = false;
private static void mesg(String s) {
if (! nomesg) {
System.out.println(s);
}
}
/** used to generate unique identifier codes */
private static int unique = 0;
/** some "large" state so that we can observe blowup */
public int[] dummydata;
private static int dummysize = 100;
public static void killAlt(int id) {
int finalizeCount = finalizeCounts.get(id);
pointers.remove(id);
while ( ! phantoms.get(id).isEnqueued())
{
mesg("(alt) trying to kill " + id + "...");
System.gc();
}
}
/** deletes the object with the given id. */
public static void kill(int id)
{
int finalizeCount = finalizeCounts.get(id);
pointers.remove(id);
while (finalizeCounts.get(id) == finalizeCount)
{
mesg("trying to kill " + id + "...");
System.gc();
}
}
// The code from these two methods can't be inlined, because
// we rely on their stack frame disappearing to prevent the
// link to the tracked object from persisting.
public static int makeTemporaryObject()
{
Immortal temp = new Immortal();
return temp.id;
}
public static void doSomethingWith(int id)
{
Immortal temp = pointers.get(id);
temp.sayHello();
}
/** identifier code */
private int id;
private Immortal()
{
id = unique++;
mesg("creating instance " + id);
finalizeCounts.put(id, 0);
pointers.put(id, this);
phantoms.put(id, new WeakReference(this, refqueue));
int last = dummysize;
dummydata = new int[last + 1];
dummydata[0] = 1;
dummydata[last] = 1;
}
public void sayHello()
{
System.out.println("hi, I'm number " + id);
}
public void finalize()
{
mesg("finalizing " + id + "...");
finalizeCounts.put(id, finalizeCounts.get(id) + 1);
// clear! *khzh-thump*
pointers.put(id, this);
}
public static void main(String[] args) {
if (args.length == 0) {
int id = Immortal.makeTemporaryObject();
// This causes the finalizer to run (in the GC thread.)
Immortal.kill(id);
// And yet, the object is still alive!
Immortal.doSomethingWith(id);
// This will now loop infinitely, since the finalizer
// will never be run a second time.
Immortal.kill(id);
} else {
for(int i = 0; i < args.length; i++) {
if (false) {
// dummy case for uniform syntax
} else if (args[i].equals("-nomesg")) {
nomesg = true;
} else if (args[i].equals("-dummysize")) {
int num = Integer.parseInt(args[++i]);
dummysize = num;
} else if (args[i].equals("-num")) {
int num = Integer.parseInt(args[++i]);
for(int j = 0; j < num; j++) {
int id = Immortal.makeTemporaryObject();
// This causes the finalizer to run (in the GC thread.)
Immortal.kill(id);
// And yet, the object is still alive!
Immortal.doSomethingWith(id);
// FSK: alternative variant of kill which uses weak references
Immortal.killAlt(id);
}
} else if (args[i].equals("-blowup")) {
int num = Integer.parseInt(args[++i]);
for(int j = 0; j < num; j++) {
int id = Immortal.makeTemporaryObject();
// This causes the finalizer to run (in the GC thread.)
Immortal.kill(id);
// And yet, the object is still alive!
Immortal.doSomethingWith(id);
}
}
}
}
}
}
Subscribe to:
Posts (Atom)