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

Require unsafe for receive operations on types with invalid bit patterns, like bool #54

Open
AndrewGaspar opened this issue Oct 28, 2018 · 7 comments · May be fixed by #79
Open

Require unsafe for receive operations on types with invalid bit patterns, like bool #54

AndrewGaspar opened this issue Oct 28, 2018 · 7 comments · May be fixed by #79
Milestone

Comments

@AndrewGaspar
Copy link
Contributor

AndrewGaspar commented Oct 28, 2018

12/6/2019: May be overzealous to make everything unsafe. Tentatively, we just need to make it unsafe to receive into types with invalid bit patterns, like bool and structs. We could potentially provide a "safe" version with a little overhead to check the output buffer.


Original issue: Mis-matching datatypes when performing communication results in undefined behavior.

Documentation should indicate that the unsafe here need not infect the whole code base. A routine that properly matches its own communications is itself safe. You only get unsafety if another routine incorrectly matches their own sends and receives. Ergo, it is possible to expose a safe interface on top of MPI communications, even if the atoms are unsafe.

See #51 for discussion on this.

@AndrewGaspar
Copy link
Contributor Author

Saw this library on HN: https://github.com/Munksgaard/session-types

Still trying to grok Session Types, but the advertising seems to be that they can provide static verification of type-safety guarantees for two communicating processes. Seems relevant.

@bsteinb
Copy link
Collaborator

bsteinb commented Aug 25, 2019

Apologies for the super long delay. If you are still interested, I think it is not necessary to mark all communication functions unsafe. I do not think that what the MPI Standard calls "erroneous" is necessarily memory unsafe. However, the Equivalence and Buffer traits are already marked unsafe and the absence of type checking of messages has implications on what kind of types Equivalence can safely be implemented for. Namely, all types that have invalid bit patterns cannot safely implement Equivalence.

@AndrewGaspar
Copy link
Contributor Author

Yeah, I'll rename this to something like "Require unsafe for receive operations on bool and other types with invalid bit patterns".

@AndrewGaspar AndrewGaspar changed the title Communication operations, both send and receive, must be marked as unsafe Require unsafe for receive operations on types with invalid bit patterns, like bool Dec 6, 2019
@AndrewGaspar
Copy link
Contributor Author

This affects #52

@jedbrown
Copy link
Contributor

jedbrown commented Feb 9, 2022

Just catching up now on session types: doesn't this mean you have to encode everything that can be sent/received when you create the pair (or group)? That seems exceedingly impractical for most MPI jobs (where the full extent of what can be exchanged is often input-dependent and may not be a finite set).

@adamreichold
Copy link
Contributor

adamreichold commented Feb 9, 2022

Just catching up now on session types: doesn't this mean you have to encode everything that can be sent/received when you create the pair (or group)? That seems exceedingly impractical for most MPI jobs (where the full extent of what can be exchanged is often input-dependent and may not be a finite set).

I think so and I basically agree with your assessment, meaning we should provide an API as ergonomic as possible even without usage of such tools.

(I suspect the practicality of using session types largely depends on how well their methods of composition work on MPI communication patterns. In some weird fantasy world, one could probably build up a session type from primitive MPI calls and then match those up (at compile time) whenever a communicator is instantiated.)

@jedbrown
Copy link
Contributor

jedbrown commented Feb 9, 2022

Yeah, I can imagine making that composition work for toy problems, but it's hard for me to see it working for real applications, say unstructured meshes and multigrid, where you end up with communication patterns (and dynamically constructed datatypes) that can't be known at compile-time. There are some collective invariants that could perhaps be enforced at compile time -- sounds like interesting research to determine if that composition is possible.

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 a pull request may close this issue.

4 participants