Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[don't merge] implement shared as references/pointers #47

Open
wants to merge 8 commits into
base: betr
Choose a base branch
from

Conversation

tjhance
Copy link
Collaborator

@tjhance tjhance commented Oct 8, 2021

The concurrency work requires shared objects to be passed by pointer/reference because of “interior mutability.” This PR adds support for it to the C++ backend.

This is not in a state for merging. It certainly requires more tests and probably could stand to have a ground-up rewrite. Also, I don't intend to spend any time cleaning this up before the upcoming deadlines, as it currently seems sufficient for the concurrency project. Still, I'm putting this up in case people are curious.

Part of the issue is that shared variables (which can be re-assigned to) must be compiled to pointer types. However, it seemed to me (originally anyway) that references would be easier to manage within expressions, seeing as they would behave the same way as non-reference types ... the result is that we have to switch to and from pointers and references in a bunch of places ... it's a mess.

The main test file is Test/c++/shared.dfy. Here's a sample:

method get_value_select<V>(shared x: Option<V>, shared y: Option<V>, b: bool)
returns (shared v: V)
requires x.Some?
requires y.Some?
{
  shared var res: V;
  if b { 
    res := x.value;
  } else {
    res := y.value;
  }
  v := res;
}
  template <typename __V>
  __V* __default::get__value__select(_module::Option <__V> & x, _module::Option <__V> & y, bool b)
  {
    __V* v = nullptr;
    __V* _149_res = nullptr;
    if (b) {
      _149_res = &( ((x).dtor_value()));
    } else {
      _149_res = &( ((y).dtor_value()));
    }   
    v = &( (*_149_res));
    return v;
  }

@tjhance tjhance changed the title [don't merge] Shared refs [don't merge] implement shared as references/pointers Oct 8, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant