Found the programming language "pony" just today... and started to play with it.
My code is supposed to do some simple producer consumer thing. As claimed by language documentation, the language ensures there are no data races.
Here, main sends 10 messages to the producer, which in turn sends 10 messages to the consumer. The consumer increments a counter state variable. Then, main sends a message to the consumer, which in turn sends a message to main in order to display the current value. If all messages were in sequence, the expected value would be 9 (or 10). The result printed, though is 0.
As this is all in hour 1 of my playing with the language, of course I might have messed up something else.
Who can explain my mistake?
use "collections"
actor Consumer
var _received : I32
new create() =>
_received = 0
be tick() =>
_received = _received + 1
be query(main : Main) =>
main.status(_received)
actor Producer
var _consumer : Consumer
new create(consumer' : Consumer) =>
_consumer = consumer'
be produceOne () =>
_consumer.tick()
actor Main
var _env : Env
new create(env: Env) =>
_env = env
let c : Consumer = Consumer.create()
let p = Producer.create(c)
for i in Range[I32](0,10) do
p.produceOne()
end
c.query(this)
be status( count : I32) =>
// let fortyTwo : I32 = 42
// _env.out.print( "fortytwo? " + (fortyTwo.string()))
_env.out.print( "produced: " + (count.string()) )
Running on windows 10, 64 bit, btw. with the latest and greatest zip file installation I found.
0.10.0-1c33065 [release] compiled with: llvm 3.9.0 -- ?
The data races prevented by Pony are the ones that occur at the memory level, when somebody reads from a memory location while somebody else is writing to it. This is prevented by forbidding shared mutable state with the type system.
However, your program can still have "logical" data races if a result depends on a message ordering that isn't guaranteed by Pony. Pony guarantees causal ordering of messages. This means that message sent or received is the cause of any future message that will be sent or received if the messages have the same destination, and of course causes must happen before their effects.
In this example,
Bwill always receive the message fromAbefore the message fromCbecauseAsends a message toBbefore sending a message toC(note that the two messages can still be received in any order since they don't have the same destination). This means that the message sent toBbyCis sent after the message sent toBbyAand since both have the same destination, there is a causal relationship.Let's look at the causal orderings in your program. With
->being "is the cause of", we haveMain.create -> Main.status(throughConsumer.query)Consumer.create -> Consumer.queryConsumer.create -> Consumer.tick(throughProducer.produceOne)Producer.create -> Producer.produceOneAs you can see, there is no causal relationship between
Consumer.queryandConsumer.tick. In the sense of the actual implementation, this means thatMaincan send theproduceOnemessages and then send thequerymessage before anyProducerstarts executing the message it received and has a chance to send thetickmessage. If you run your program with one scheduler thread (--ponythreads=1as a command line argument) it will always printproduced: 0becauseMainwill monopolise the only scheduler until the end ofcreate. With multiple scheduler threads, anything between 0 and 10 can happen because all schedulers could be busy executing other actors, or be available to start executing theProducers immediately.In summary, your
tickandquerybehaviours can be executed in any particular order. To fix the problem, you'd have to introduce causality between your messages, either by adding round-trip messages or by doing the accumulating and printing in the same actor.