Improve documentation of Unix.{in,out}_channel_of_descr

[xavierleroy]

As discussed in #9786: this PR documents more precisely what to do and what not to do in order to close the channels created with Unix.{in,out}_channel_of_descr fd and the underlying descriptor fd.

[gasche]

The sentence is confusing: "and of" and "several" are not so clear to me. Maybe it would be clearer to be more redundant:

If several channels are created on the same descriptor, you should either close one of the channels (but not the others nor the descriptor) or close the descriptor (but none of the channels).

[xavierleroy]

What's wrong with "channels ⋃ {descriptor}" ? :-)

I simplified the explanation by omitting to mention that the descriptor can be closed. It's not the best solution anyway.

[gadmm]

The text looks good and is a very helpful clarification; I agree with your analysis of the situation. I would add a couple of words to clarify that open_connection and establish_server give a pair of channels on the same descriptor (no other functions seem unclear in this way).

But I disagree that "you can close the file descriptor, just do not use the channel afterwards" is a fair advice to give to programmers. When one does so, the value is placed in an invalid state where further operation (a bug) can fail properly with an exception on good days, but it can also fail silently with an unpredictable outcome. Even assuming that users will follow simple patterns to avoid use-after-free, simple code evolves and becomes more complicated over time, use-after-free can be introduced at a distance, the escaping of borrowed resources gets more tricky to prevent with some monadic styles, etc. It gives bugs that are hard to notice and debug. Instead, we need an operation that properly closes the channel without closing the descriptor, as described at #9786 (comment) (which cannot currently be written).

[gadmm]

Further points, if I am not mistaken:

• If one somehow forgets to flush a out channel but closes the descriptor, then the failure semantics is very bad since nothing happens at the moment but during program exit the channel will be flushed to a bogus fd.
• Not closing a named channel causes a runtime warning during finalisation. This is not the case with the channels obtained with *_channel_of_descr, but the user might wrongly generalise the advice to channels independently of how they are obtained (given that the file descriptor can always be obtained with descr_of_*_channel). I find your wording very careful, but I still imagine programmers missing the fine prints.

[xavierleroy]

Thanks @gadmm and @gasche for the feedback.

I would add a couple of words to clarify that open_connection and establish_server give a pair of channels on the same descriptor (no other functions seem unclear in this way).

Good point. Done!

But I disagree that "you can close the file descriptor, just do not use the channel afterwards" is a fair advice to give to programmers.

Agreed. Especially for output channels, where it can lead to data loss if the channel wasn't flushed properly.

I simplified the explanations to just say "close the output channel, don't close the underlying file descriptor, and if there is also an input channel opened on this descriptor, leave the input channel alone". This should be pretty error-prone.

[jhjourdan]

I agree that the new text is better, but I still have a few remarks.

[jhjourdan]

Actually, this is an undefined behavior, since the file descriptor may be reused in between. We cannot guarantee thet there is an exception raised here.

[xavierleroy]

All right, I just put "It is incorrect to close both the channel [ic] and the descriptor [fd].". Sometimes the less you write the better.

[xavierleroy]

The time we can collectively spend on this tiny issue has reached zero, so I'll merge now. Thanks for all the discussions.