DavidJ, I know that was mainly a question for Shap, but I have a few points which might be useful:
The way I interpret Shap's point is that we don't know yet if zero-pause GC is good enough for _all_ programs, or even all those programs which would otherwise use C and C shlibs. It's probably a lot closer than stop-the-world GC, but it's too early to put all our eggs in that basket. At any rate, maybe a typesafe runtime for all programs is not the right goal. For starters, if zero-pause GC turns out to be unacceptable for some programs, then we have no evidence that the goal is attainable. Further, even if it is, it's restrictive; not all applications need GC. For example, those programs which can be shown to be safe just using region typing should not be using GC. But of course, we want to be able to build a system out of components that use GC and components that only use region-typesafe allocation. More generally, we want to be able to build a system out of components that use all sorts of memory management policies. The problem then is that anyone could come up with a new and reasonable memory management policy at any time, and we'd want to be able to integrate it. So any "fixed-function" runtime with a fixed set of memory management policies it integrates will be insufficient sooner or later. This is more obviously true when you consider the more general problem of storage management which includes filesystems and databases, including those split among multiple servers. Ideally, programs that deal with all that should be demonstrably safe too. But if our runtime is so extensible that new memory management policies can be added and used, then type checking (as it's usually understood) using a fixed type system is not strong enough to guarantee safety of the resulting integrated system. So here are the options I see: - Live dangerously: Use various tricks to demonstrate the safety of _some_ programs, with some remaining amount of low-level unsafe infrastructure. - Compromise: Settle on some typesafe runtime and shoehorn as many programs into it as practical. - Formal verification: Basically like "live dangerously" in that it uses as many tricks as possible to provide simple safety arguments, but instead of defaulting to unsafety, it defaults to a machine-checkable proof using formal models and general-purpose logic. If you want a typesafe runtime to replace C, then you are essentially saying we should write all programs on top of some fixed runtime. In other words, as I see it, you are asking for compromise. But you have argued yourself that essentially people turn to C (live dangerously) when they find the compromise option to be unacceptable, currently because of GC pauses. So with your proposed system based on zero-pause GC, the unacceptable compromise would be something else, but it would still exist (due to the inherent restriction of type-safety arguments), and it would lead some programmers (probably far fewer) back to C or some other unsafe infrastructure (in which case, why not C?). In summary, I think zero-pause GC is promising, and a safe runtime that uses it could be extremely popular, but it will not replace C. So if the (much-better) compromise of a typesafe, zero-pause GC'ed runtime is OK with you, then you are essentially right, but should probably de-emphasize replacing C. If you really want to replace C, your killer app is end-to-end system safety proofs, and you want formal verification (upon which type safety can be proven and used), because type checking alone is not flexible enough. I originally got interested in BitC because I thought its design goal was to be a practical substrate for formal verification. (I don't think C is a practical substrate because hardly anyone completely follows the C spec anyway.) But now it seems like Shap is pursuing the "live dangerously" option, but trying to make it less dangerous using strong, low-level types. All this is to say: I would summarize your difference in opinion by saying Shap is trying to make "live dangerously" less dangerous, and DavidJ is trying to make "compromise" a more realistic compromise. To restate again, you're both approaching the ideal of a safe, universal systems language, but from different directions. Shap wants to make languages safer while guaranteeing universality. DavidJ wants (I think?) to make languages (and runtimes) more universal while guaranteeing safety. And as I said before, I don't believe the ideal (safe, universal language) can be reached without some amount of formal verification. On Fri, Apr 13, 2012 at 4:19 PM, David Jeske <[email protected]> wrote: > > On Apr 13, 2012 10:10 AM, "Jonathan S. Shapiro" <[email protected]> wrote: >>> After we have a zero-pause runtime, we can spend time and research on >>> alternative techniques such as regions and advancements to value-types to >>> relieve pressure on the GC system. >> >> That's backwards. The region and other advances are available to us today. >> The pausless collectors are still not understood well enough to be >> mainstream yet. > > I'm working on a longer response to some other points, but i think this > divide above deserves some digging into on both sides. Here is my reasoning. > Im very interested to hear yours. > > If our goal is a typesafe systems runtime to represent all programs (i.e. a > replacement for c and c-shlibs), we need a general purpose typesafe heap > memory reclamation scheme. Regions, refcounting, and linear-types _alone_ > can not represent all programs. Thus, if we wish to create a typesafe > runtime to represent all programs, these solutions can only serve as an > optimization for a subset of such a system. They can only represent all > programs by combining them with manual-management (which is not typesafe) or > gc (which brings us back to my point). > > The only type-safe heap reclamation schemes im aware of which are capable of > representing all programs are (a) some variation of mark-sweep-compact > tracing gc, and (b) ref-counting, with some variation of mark-sweep cycle > finding. Therefore, one of these two schemes is a good candidate for the > base of a typesafe runtime (once it meets our no-pause/low-jitter > requirement) to replace c/shlibs/malloc, wheras regions et. al. are only > suitable as optimizations within such a system. > > What is your argument? > > Do you believe regions and such are capable of representing all heap > reclamation needs and we simply don't know how? It seems to me any other > argument devolves into gc or manual management, which simply proves my > point. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
