larus wrote:
Language Support for Fast and Reliable Message-based Communication in the Singularity OS, Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James Larus, and Steven Levi, EuroSys 2006 Conference, pp. 177–190.



Hi everyone,

I hope this thread is still active.
I have read the above mentioned paper and I got some questions about it:

1. In the example with the methods Consume(vec) and Reverse(vec) you mentioned that it would result into an access error if Consume(vec) happens before Reverse(vec), which is clear since after the execution of method Consume(vec) the tracked vector is no longer available for Reverse(vec).

But: Is the compiler still able to verify the following code?

if(...) {
  Consume(vec);
}
Reverse(vec);


or


if(x > 0) {
  Consume(vec);
} else {
  Reverse(vec);
}
if(x <= 0) {
  Consume(vec);
}


The first example is only safe, when the if branch isn't executed.
The second example is actually type safe, but according to the paper "Enforcing High-Level Protocols in Low-Level Software" by Robert DeLine and Manuel Fähndrich the type checker will reject it. I think the verification main idea is actually the same in Sing# as in Vault.
In Vault's type system the programmer has to use keyed variants to fix this problem? How is this done in Sing#?

2. In the paper you mentioned that Channels on Singularity outperform the mechanismns available in Windows/Linux/FreeBSD by the factor of 4 to 5. You also state that this improvements don't even factor in the ability to pass pointers rather than copies of memory blocks. So, from what does this result from? Does it have to do with the expensive system calls in the other systems?