Fix SHARING behaviour

[reuk]

This PR fixes up the behaviour of SHARING so that it can be disabled if necessary. I think the way that SHARING is currently used could be improved - see for details. #907

[peterschrammel]

Maybe add a Fixes #907to the commit message body.

[martin-cs]

Thinking about it; do we need the SHARING macro at all? I'm not aware of anyone using the non-shared version in the last 5 or so years. Given how important it is for performance I'm hard pushed to think of why anyone would want a non-sharing version. Maybe to debug issues in the sharing code? But the only one of those we had recently we didn't use this so I'm not convinced.

[tautschnig]

I tend to agree that, if anything, we need more sharing. @kroening to decide whether SHARING should just be the default and all other approaches be removed.

[reuk]

Recently I've been turning off sharing when looking for memory leaks (which is why I thought I should submit this patch). Even if a particular leak isn't due to reference cycles through irept, it's nice to be able to ensure that it isn't. On the other hand, I'm in favour of reducing the number of different build configurations in general, and it would make the code a lot cleaner to just remove the non-sharing option.

[martin-cs]

On Mon, 2017-05-15 at 00:23 -0700, Reuben Thomas wrote: Recently I've been turning off sharing when looking for memory leaks (which is why I thought I should submit this patch). Even if a particular leak isn't due to reference cycles through `irept`, it's nice to be able to *ensure* that it isn't. On the other hand, I'm in favour of reducing the number of different build configurations in general, and it would make the code a lot cleaner to just remove the non-sharing option.

If you are getting value from it being there then it can stay. I just hadn't seen anyone else use it in a while.