Make message::get_mstream const

[LAJW]

Changes message::mstream object to mutable so that message::debug()
and its friends can be run by constant methods.

Warning: in the future, when implementing multiple threads,
implementation of get_mstream will have to be changed so that each
thread has its own, local standard output. As it stands each
get_mstream() call changes stream type for the whole program.

[tautschnig]

Warning: in the future, when implementing multiple threads,
implementation of get_mstream will have to be changed so that each
thread has its own, local standard output. As it stands each
get_mstream() call changes stream type for the whole program.

Isn't this the explanation for why the proposed change should not be made?

[LAJW]

@tautschnig

Isn't this the explanation for why the proposed change should not be made?

It's already broken, even for single threads. For example:

auto& stream1 = debug();
auto& stream2 = error();
stream1 << "this is printed to error stream";
&stream1 == &stream2 // true

The problem is that calling those stream methods toggles to which output the main global stream is printing. get_message() should return references to unique objects, rather than switch internal state. Similar pattern occurs everywhere else. But that's a larger architectural problem.

[tautschnig]

So what's the reason for this PR? (The commit message explains what is being changed, but doesn't cover the "why". See also https://chris.beams.io/posts/git-commit/ and specifically "7. Use the body to explain what and why vs. how".)

Edit: why is it desirable that the methods "can be run by constant methods."

[LAJW]

so that message::debug() and its friends can be run by constant methods.

Isn't this why? There are many methods in child classes that should be const but aren't, just because they are using a debug() method somewhere. Const methods are easier to reason about and may be faster as the compiler has easier time optimizing them.

[tautschnig]

There are many methods in child classes that should be const but aren't, just because they are using a debug() method somewhere. Const methods are easier to reason about and may be faster as the compiler has easier time optimizing them.

So why is it correct that they should be const? After all the use of debug() does modify the state. (I do have an answer in mind that justifies your use of mutable, but I'd like to hear your take on this as well.)

[LAJW]

My take is that these methods should not be a part of the solver object. The stream object (or its reference) could be stored there for convenience. In addition rather than having a switch that redirects streams, this sub object should contain a set of discrete stream outputs, just like std::cout, cerr, etc.

[tautschnig]

You seem to be arguing about a larger design change. I'm not saying this is wrong, but I don't see how this justifies that "mutable" is correct here.

[LAJW]

I am not arguing for changing it right now, but just laying out a change that would fix past and current issues with the stream object. Since it's slightly architectural, I'm not pushing it now, just providing a temporary practical fix.

[tautschnig]

What I am challenging here is whether the use of mutable is safe at all!?

[LAJW]

Yes, because solvers are not multi threaded.

[tautschnig]

I don't think multi-threading is a necessary condition for mutable to break anything. Even in a single-threaded system the modification of objects assumed to be const can cause havoc. So why is this not the case for this pull request?

[LAJW]

Solvers aren't const. And this method is part of the solver object.

[tautschnig]

But then you mentioned there are methods you'd like to mark const (as otherwise this entire PR is unncessary?) -- so why would it be safe to mark them const when the streams are mutating?

[LAJW]

Calling const method on a non-const object is safe. Same thing with copying shared_ptr being const operation, even though it mutates its reference counter.

[tautschnig]

Like this?

#include <cassert>

struct S
{
  void safe() const
  {
    m=0;
  }

  mutable int m=42;
};

int main(int argc, char* argv[])
{
  S s;
  assert(s.m==42);
  s.safe();
  assert(s.m==42);
  return 0;
}

[LAJW]

Yup. Even with -O3 it works as expected - second assertion fails because s.m is set to 0. There's no reordering going on.

Now, ideally the class invariant shouldn't be changed - so mutable should be used mostly for reference counting, mutexes and caching. In the case of my pull request is to circumvent a badly designed interface.

I could create 7 discrete stream objects and set stream type of each in the constructor once for the entire duration of the program. That way no mutable keyword would be required. I am not sure whether such change would be accepted though.

[tautschnig]

Even with -O3 it works as expected - second assertion fails because s.m is set to 0.

Well, the question is just what is "expected" - calling a const method the user may expect nothing would change. What I do ask you to put forward is a rationale for why it will all work "as expected" with this PR applied. As a hint: what do "reference counting, mutexes and caching" have in common?

[LAJW]

what do "reference counting, mutexes and caching" have in common?

This question was already answered in my previous comment.

Here's a branch with streams implemented correctly (discrete streams): https://github.com/LAJW/cbmc/tree/discrete-streams
Problem is: some code depends on state-changing behaviour of stream() calls and would have to be upgraded accordingly.

[tautschnig]

This question was already answered in my previous comment.

Would you mind copying that answer - I couldn't find it.

(Yes, I'm being pedantic. But code correctness is key.)

[LAJW]

Now, ideally the class invariant shouldn't be changed

[tautschnig]

I'd refer to the programmatically observable part of the state, which may include class invariants. Specifically, streams cannot be (or maybe just "are not being?") publicly read from. (The same holds for the examples you mentioned.)

[peterschrammel]

Then the question is whether we consider message streams to be observable from within the program. I tend to say 'no' even though this is in conflict with the strict meaning of 'const'.

[reuk]

This seems to just affect whether the mstream is treated as part of the "logical state" of the object. This is fine in isolation, but suggests the need for further changes/refactoring in the future. It certainly seems as though the stream shouldn't be part of the object's logical state, which in turn makes me think that it shouldn't be part of the object state at all.

[tautschnig]

Closing as merged into develop with "master" no longer being updated.