On Tue, Jul 30, 2013 at 3:37 PM, David Jeske <[email protected]> wrote:

> On Tue, Jul 30, 2013 at 2:49 PM, Jonathan S. Shapiro <[email protected]>wrote:
>
>>
>>
> A really interesting alternate path would be to design CLI/CLR' and
>> proceed from there. The three interesting questions in that would appear to
>> be: (1) what does the type system look like, (2) what concurrency
>> deficiencies do we want to resolve, and how, (3) what does the new GC look
>> like. The main thing that stops me from going there right off is that I
>> think that type system is informed by our HLL type system requirements.
>
>
> I'm interested to know more about your thoughts on concurrency. I agree
> it's a challenging space. So far I view shared-nothing concurrency models
> like you view checked-exceptions, where the curse is worse than the
> disease.
>
> Are there any particular papers or posts I can read about your
> bias/leanings?
>

No. Mainly because, as I say, I don't know enough about concurrent
programming to feel like I have an informed opinion. The only concrete
experience I have with concurrency is in the Coyotos kernel. *That* one is
such a special case that it would be pretty silly to do language support
for it. The system is transactional to begin with, which makes it
few-of-a-kind, and all paths to commit/abort are short enough that eager
lock release only makes sense on the ready queue. There was only one place
where any sort of dance involving carefully ordered lock and release was
required. That one was on the ready queue, and occurs in some variation in *
every* operating system kernel. Those statements, taken in combination, let
us design a custom locking system that *hugely* simplified everything, and
simultaneously let us bound priority inversion.

In the context of BitC, I've thought about two kinds of things:

1. Typing support for deep immutability. It would be really useful to know
which subgraphs are deeply immutable and therefore can be accessed
concurrently without any locking at all. It's even possible to imagine
schemes in which phase changes are possible in both directions between
normal and deeply immutable states. This helps a lot in some fork/join
style concurrency, but it's certainly not a cure-all.

2. Lock labeling (which I sometimes think of as lock regions). In Coyotos,
we had very careful discipline about which slots were governed by which
locks. In most cases the lock was embedded in the object, but not in all.
Notably, there were some hash tables in which the proper lock is found by
applying a deterministic function to the object identity. It seems mostly
possible to document the relationship between locks and the things they
govern by suitable labeling, and to use some form of acquire/release
discipline to ensure that locks are acquired before their associated fields
are sourced or mutated. Separately, it seems straightforward to label those
fields that can only be sourced/sinked by CAS or atomic operations.

Note that this isn't enough to make things concurrency safe. It *may* be
enough to help the programmer ensure that appropriate lock relationships
exist and have been acquired. It's definitely *not* enough to let us reason
sensibly about wait-free data structures. I'm not sure what annotations
would be appropriate for that, and I'm not sure how to check them. I'm
aware that some promising work exists in the research literature; I just
haven't had a chance to dig in to it.

I'm guardedly hopeful that if we could get these two things covered, then
we can build a fairly wide range of concurrency solutions as library code,
supported by appropriate typing constraints. Might not cover everything,
but it would cover a whole lot of things.

3. As I've said more recently, I'm fairly convinced that we need intrinsics
to deal with memory access barriers so that we can write checkable
concurrent programs in the presence of weak memory ordering. I'm not sure
how that should be expressed. It seems possible that lock labeling might be
enough to let us do it automatically if lock labeling really works out.


But that's about the extent to which I've pushed into this. Getting a
satisfactory sequential semantics going first seemed like the right place
to start.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to