Munksgaard / session-types

MIT License
549 stars 21 forks source link

Destructor bomb #22

Closed Munksgaard closed 8 years ago

Munksgaard commented 8 years ago

Introduce destructor-bombs to improve the (runtime) safety of the library.

Manishearth commented 8 years ago

It may be possible to avoid using the extra bool field by prematurely running drop (manually) in close(), like so

This means we would have to do the following in close():

fn close(mut self) {
 // create some dummy values to place inside
 // this is safe because nobody will read these
 let mut sender = unsafe { mem::uninitialized() };
 let mut receiver = unsafe { mem::uninitialized() };
 // extract the internal sender/receiver so that we can drop them
 mem::swap(&mut self.0, &mut sender);
 mem::swap(&mut self.1, &mut receiver);

 drop(sender);drop(receiver); // drop them
 mem::forget(self); // Ensure destructors don't run
}

The implementation of mem::swap uses the same combination of creating an uninitialized() scratch space and forgeting it before it can get accessed.

Sadly, we cannot move out of types implementing destructors, otherwise the above impl could just destructure and drop the components. Instead, we have to do some trickery.

Munksgaard commented 8 years ago

That is certainly another possibility. It keeps the Chan implementation simple, but perhaps your implementation of close would throw some people off? Also, do you have any ideas what the performance would be like?

Manishearth commented 8 years ago

Just leave an elaborate comment and it should be fine.

It's not inefficient; we do the same thing drop() does (without calling Drop::drop()), and we additionally allocate stack space for a dummy sender/receiver pair. Not heavy at all.

Munksgaard commented 8 years ago

Cool. Do you wanna do a PR?

Manishearth commented 8 years ago

Updated this one

Munksgaard commented 8 years ago

Before we merge this, I think we should make sure that it wont hinder @laumann's port of Servo too much (https://github.com/laumann/servo/tree/session-types). Obviously, destructor-bombs like these shouldn't have an impact on correctly designed programs, but because the Servo port is the main use case of this library so far, it'd be nice to actually see it work before we merge.

laumann commented 8 years ago

In the Servo code I've taken great pains to properly close channels (and have considered it an error when this didn't happen).

EDIT: But yes, I agree that it would be nice to see it working before we go all in...

Manishearth commented 8 years ago

That can't stop the destructor from running. Moving it to compile time requires linear types, which Rust doesn't have (not counting humpty_dumpty, which is an approximation)

Manishearth commented 8 years ago

The thing is, even with a protocol-complete marker, you can't force folks to reach that marker in highly concurrent code (we can't just wrap it in a function like above because the protocol may be enacted over many steps via structs and stuff, and branch off).

Munksgaard commented 8 years ago

Hi @setir, thanks for contributing :smile:

That is definitely an interesting idea, and one that was somewhat suggested at our recent presentation of the library at WGP.

As I understand it, your idea is somewhat similar to having a function like the following

fn start_session<P: HasDual>(Fn(P) -> Eps, Fn(P::Dual) -> Eps)

instead of the session_channel() function that we provide. That is, a function that takes two functions as input, and runs them as the opposite sides of a session, requiring that both return Eps (or Completed).

I agree that this would ensure that both protocols run to completion, but I believe the lack of flexibility would cause some problems for us. For instance, It would become much harder to set up more complex communication networks: How would you set up a network consisting of three processes all talking to each other using only start_session? The way I see it, you would almost certainly need to rely on other primitives, like Rust's builtin channels, because start_session only supports two processes at a time.

Munksgaard commented 8 years ago

@laumann: Let's merge this as well, shall we?