Using unsafePerformIO safely?

#54

Sorry @atravers I didn’t quite get the intent; so you agree that it’s a useful/legit use case in this context, don’t you?

#55

I agree with this, but I’m not certain that it’s enough. The problem here is that words like “side effect” imply some kind of abstraction boundary between things that the program should care about, and things that it should not. Without that abstraction boundary, nothing can ever satisfy the conditions to be safe.

In this example, invoking an SMT solver can definitely have side effects if other parts of the program look at the list of running processes to decide whether the SMT solver is running. Does that matter? Most of the time, probably not… but it certainly does matter if you’re using the SMT solver as part of a program that enforces a policy on how many processes a user is allowed to run!

For this reason, I reach the conclusion that Richard’s hypothetical ProofOfSafety is fundamentally impossible to define as part of a general-purpose library, because it relies on decisions about how to draw the right abstraction boundary, and that decision varies from program to program.

#56

Note that the side effects must be observable from pure Haskell code. You cannot access the list of running processes that way.

Inside IO you can monitor everything that happens on the computer, so otherwise everything would be a side effect. Even 1 + 1 would have the side effect of taking time to compute and running instructions on your CPU, which you can observe inside IO.

#57

Huh. So even the oft-quoted launching of the missiles, the most famous example of a side effect, isn’t a side effect in your view? This seems far too restrictive a notion of side effects. Now basically anything, no matter how unsafe, qualifies as technically “safe” because you cannot observe it from pure code.

Yes, this is basically what I said. If you fail to draw an abstraction boundary between internals and exposed behavior, then there is no such thing as safety. In practice, we don’t define that boundary formally. We just all sort of know that the time it takes to compute a pure expression isn’t thought of as a side effect, whereas launching missiles typically (but I guess not always!) is. If you want to prove anything, you’d need to be quite explicit about the boundary.

#58

I guess so. I would consider anything that can’t come back to influence the actual evaluation is not really a side effect (that we should care about).

Consider (what feels to me like) the dual: reading something from the “outside world” that is a static value, i.e. not influenced by anything else in the environment. I believe that is a common use case of unsafePerformIO in practice, e.g. Control.Concurrent.rtsSupportsBoundThreads (this actually uses the FFI and not unsafePerformIO directly).

#59

I was just providing some examples of where “regular” monadic I/O (which is strict) is too restrictive - then again, perhaps I didn’t quite get the intent of @tomjaguarpaw’s remark…

so you agree that it’s a useful/legit use case in this context, don’t you?

In this context (and in the absence of a practical alternative): yes - as much as lazy I/O is despised, sometimes you need that laziness. Yes, such a mechanism has its problems, but then so does regular I/O e.g:

import System.Process(getCurrentPid, callCommand)

main = do pid <- getCurrentPid
          callCommand $ "kill " ++ show (toInteger pid)

Programming today is a race between software engineers striving to build bigger and better idiot-proof programs, and the Universe trying to produce bigger and better idiots.

So far, the Universe is winning.

Rich Cook.

#60

…unfortunately our reality isn’t quite so “neat and tidy” - a Roman candle could go off-course and land where the computer running the Haskell program in control of the fireworks is located. Even reading in a static value can have an effect e.g. changing the access time of a file.

To me, this topic is just another aspect of I/O, and it continues to confound:

  • otherwise there wouldn’t have been calls for more "semantically simple" alternatives

  • …and this thread wouldn’t have attracted so much attention :-)

Getting back on-topic: a guide for the safe safer use of unsafe entities (even if it is a draft version) is probably the best that we can do for now, hence the inquiry. It would surely be a small improvement of the current situation where such advice, if it exists, is scattered throughout cyberspace…

1 Like
#61

Nice, I completely agree.

tl;dr: Basically here they are making a cheap, thread-safe “queue” of IO Reply actions without the need for a “canonical” queue-like data structures (Chan, TQueue…) I have not benchmarked this but I can only assume it blows these alternatives out of the water.

#62

Luckily, you can’t observe roman candles destroying your computer or file systems changing access times from within pure code.

#63

Since pure code also cannot observe the side effects of their use, wouldn’t that imply unsafe I/O entities can be used anywhere?

#64

No, you can do some things that are observable, e.g.:

ref = unsafePerformIO (newIORef True)

set x = unsafePerformIO (writeIORef ref x)
get = unsafePerformIO (readIORef ref)

On their own get and set are relatively harmless. And the ref is even a common practice. But having the ability to both set and get a mutable value means that you now have the ability to observe the effects.

Similarly, you could imagine having an SMT solver function and having a function that gets the list of running processes, both using unsafePerformIO. The latter can observe the effects of the former, so this is unsafe. Also, in this situation the list of running process probably changes all the time, so that is a problem all on its own.

#65

…harmless or useless?

  • ref = return ()
set _ = return ()

  • ref = return ()
get = return True

Consider the situation where that SMT solver and working-process monitor are in two separate third-party libraries: by themselves in each library, their effects are “benign”. But what if you need those two libraries in your new program?

Now imagine if every library could potentially have its own "benign" use of an unsafe I/O entity…

1 Like
#67

True, to get modularity, modules have to communicate which assumptions they make about the use of unsafePerformIO in rest of the program.

Then it makes sense to make an explicit model of the larger system and to use that to specify which things you consider side effects. For example, do you consider creating a new process a side effect or not? In that sense @cdsmith’s suggestion above seems more principled and modular.

Now I’m also wondering, a use of unsafePerformIO that is often considered safe is if all the side effects are encapsulated. For example, if you deallocate or freeze all mutable arrays before leaving the scope of unsafePerformIO. Or in the process example, if the process finishes before leaving the scope of unsafePerformIO.

One problem with that is that the created process might still be observable if other code is running concurrently.

1 Like
#68

 

Unfortunately, those assumptions would need to be pessimistic by default because of transitivity: a definition in one module can indirectly depend on a definition in another which uses unsafePerformIO. For most codebases, that could end up “tainting” many modules, quite possibly the majority of them.

It would then probably be easier to just assume the worst - that any module can be tainted - and not bother with those communications.

That resembles the “safe-usage” requirements for unsafeLocalState:

…perhaps this is as close as anyone will get for now to a guide for the safe use of unsafePerformIO.

1 Like
#69

The question “when do we know that unsafePerformIO is safe” can be specialized to “why do we believe that runST is safe?” (which is one possible use of unsafePerformIO).

I asked that before, and shortly after an answer was given by Amin Timany et al in their POPL 2018 paper “A Logical Relation for Monadic Encapsulation of State”.

So that establishes one possible way of answering that question. I am not sure how easy it is to extend to other uses of unsafePerformIO (e.g. the tricks I am playing here), or to safety in the presence of concurrency.

2 Likes
#70

Correct.

The problem is observable effects:

  • ST actions like readSTRef and writeSTRef only manipulate the contents of the program’s memory - usually only made visible with a debugger.

  • however, IO actions like getChar and putChar work with I/O devices which can potentially manipulate anything, including the program itself.

As for safety with concurrency, everyone’s favourite “type-smith” has already shown how unsafeInterleaveST (and consequently unsafeInterleaveIO) breaks regular Haskell semantics, even though their results are monadic:

unsafeInterleaveST :: ST s a -> ST s a
unsafeInterleaveIO :: IO a -> IO a

as opposed to:

unsafePerformST :: ST s a -> a
unsafePerformIO :: IO a -> a

If only there was a denotative way to write system software…

Looking back to that denotative future
#71

Is anyone surprised that unsafeInterleaveST can be used to break semantics? That’s why it’s called unsafe… But certainly some uses of it are ok, and we are back to the original question of how to prove that that’s the case (or even what exactly “that” means).

#72

Is anyone surprised that unsafeInterleaveST can be used to break semantics? That’s why it’s called unsafe…

Originally it was just named interleaveST (see page 10 of 12). I’m guessing that because it was for encapsulated state rather than general I/O, some may have thought it was safe. But something must have annoyed Oleg enough to devise his counter-example…

But certainly some uses of it are ok, and we are back to the original question of how to prove that that’s the case (or even what exactly “that” means).

Because of Rice’s theorem, such a non-trivial semantic property cannot always be proven - it could be possible to check for safe usage in certain circumstances, but as for the rest: we’re back to using heuristics and due care.

(If economics is the dismal science, then what are we to make of computer science?)

#73

I think what a side-effect is depends on what the observer is interested in when running the program. In an operational semantics, you would perhaps make such side-effects explicit by labelling certain kinds of transitions with an Event such as “asks for a new ref cell”, “reads from a ref cell”, “launches missiles”, “terminates” etc.

Over the course of the program execution, the observer can collect these events and then compare the event log of different traces. If the observer decides that ref cells are boring, then the new, read and write events aren’t a side effect and hence not collected. (The decision not to care for ref cells might still make a difference when one trace launches a missile when the other doesn’t simply because of different contents of a ref cell. Which is pretty much why Haskellers consider reading and writing to ref cells a side-effect.)

See also What is a good formal definition of purity? - #21 by sgraf in that regard.

If the observer doesn’t care whether the SMT solver is run and the result of doing so isn’t otherwise observable compared to running a pure function instead, then it’s not a side-effect. By contrast, if the SMT solver reads and writes non-existant configuration files and whatnot, the observer often questions whether the program is actually free of side-effects.

2 Likes
#74

Unfortunately, there’s no reliable way to tell if the SMT solver (or any other foreign entity) is going to be “well-behaved” or not when it’s used: