> Deadlock-Free: This one is easy because Pony has no locks at all! So they definitely don’t deadlock, because they don’t exist! This really annoys me every time I read Pony description. What does deadlock free even mean here? Deadlock-free is typically the property of an algorithm, not a language.

Does pony guarantees forward progress in all cases? Does it means that if I tried to implement a python interpreter in Pony it will statically reject the implementation? Requires me to submit a proof of deadlock freedom with any program I feed the interpreter? Or any python program running on this interpreter is magically free of deadlocks?

edit: as an aside, deadlocks have little to do with locks.

▲

BlanketLogic 4 days ago | parent | next [-]

It is based on actors and "reference capabilities". These two blogs[1,2], could provide nice introduction.

1. https://blog.jtfmumm.com//2016/03/06/safely-sharing-data-pon... 2. https://bluishcoder.co.nz/2017/07/31/reference_capabilities_...

▲

gpderetta 4 days ago | parent [-]

That's quite interesting, but it doesn't answer the question: Would the python program running on an interpreter written in pony deadlock or not?

▲

gf000 4 days ago | parent [-]

It would livelock

▲

gpderetta 4 days ago | parent [-]

I wouldn't call it a livelock, because I wouldn't expect the runtime to be doing any (useless) work on behalf of the program.

Still, trading deadlocks for livelocks is a net negative as they are harder to identify and diagnose.

	▲	senderista 4 days ago \| parent [-]
		Paxos necessarily livelocks and still seems useful. More generically, all nonblocking algorithms which are only “obstruction-free” can livelock, but techniques like randomized backoff can make them quite reliable in practice (just like Paxos/Raft).

▲

unbrice 4 days ago | parent | prev | next [-]

It would be technically deadlock free because you'd have a state that is unable to progress forward but it wouldn't technically involve a synchronisation primitive. In my view a real deadlock would actually be easier to debug but I'm just a caveman.

	▲	4 days ago \| parent [-]
		[deleted]

▲

rurban 3 days ago | parent | prev | next [-]

Of course it cannot guarantee forward progress in all cases, because that would be NP.

Pony guarantees deadlock freedom by eliminating locks and other mechanisms that can lead to deadlocks. Instead, Pony uses a message-passing concurrency model and static analysis to prevent data races and deadlocks at compile time. This means developers don't need to worry about manually preventing deadlocks because the compiler handles it. The scheduler is lock-free, the order of message-delivery to all actors is guaranteed.

Here's a more detailed explanation:

Message-Passing:

Pony employs a message-passing model where actors (objects) communicate by sending messages to each other. This avoids the need for shared mutable state and locks, which are primary sources of deadlocks.

Static Analysis:

The Pony compiler performs static analysis to ensure that concurrent access to data is safe. It prevents data races and other concurrency issues that could lead to deadlocks by verifying that no two actors can simultaneously write to the same memory location.

No Locks:

Because Pony doesn't use locks, there's no possibility of threads getting stuck waiting for each other to release locks, which is a common cause of deadlocks.

Data Race Freedom:

By eliminating the possibility of data races (concurrent modification of shared mutable state), Pony also eliminates a major source of potential deadlocks.

	▲	thayne 3 days ago \| parent \| next [-]
		> Because Pony doesn't use locks, there's no possibility of threads getting stuck waiting for each other to release locks, which is a common cause of deadlocks. It may be a common cause of deadlocks, but it isn't the only way to have deadlocks. A book I read on erlang had an entire chapter on how to avoid deadlocks with actors that had several examples of how you can get a deadlock with just message passing. In fact, it is possible to implement a lock/mutex (also a semaphore) with actors and message passing.
	▲	gpderetta 3 days ago \| parent \| prev [-]
		sorry, that's nonsense, you can trivially deadlock without mutexes with message passing. edit: and to be clear, I'm quite interested in Pony, static typing, shared nothing threading with message passing, capabilities, per thread GC is very close to my ideal programming language. But the bogus deadlock-freedom claim make me question the other claims.

▲

perching_aix 4 days ago | parent | prev [-]

> Does it means that if I tried to implement a python interpreter in Pony it will statically reject the implementation?

How could that be true? You'd be emulating the language particularities, so deadlocks would be just virtual states. Your interpreter itself being free of deadlocks doesn't mean it cannot represent them.

It's like thinking that you cannot write e.g. console emulators in Rust, because people typically ship unsafe code to consoles, yet Rust enforces memory safety. Yes, it does enforce it - so you'd be representing unsafe accesses instead, rather than actually doing them.

▲

gpderetta 4 days ago | parent [-]

Well, yes, that's my point. So what does it means that Pony is deadlock-free?

▲

unbrice 4 days ago | parent | next [-]

It means that the language and runtime both agree not to look at your dead-end state, so no-one can say it's their fault ;)

For example I can define a notsemaphore actor that calls a callback once an internal count reaches 0, and then I can forget to decrement it and so it will never reach 0. But technically this didn't involve synchronization so there isn't a stack trace to tell me why is my program stuck and somehow this is better.

	▲	gpderetta 4 days ago \| parent [-]
		As someone that has spent the last week debugging a possible deadlock in pure async message passing code, I'm not amused :).

▲

perching_aix 4 days ago | parent | prev [-]

That the logic you implement directly in Pony is deadlock-free. If you implement something that can represent arbitrary logic / represents deadlocks, then you get deadlocks again. This extends to every constraint-like language feature ever in any language.

▲

gpderetta 4 days ago | parent [-]

Ok, partially evaluate the interpreter against a python always-deadlocking program. Now it no longer implement arbitrary logic, but it is a very specific program. Yet it deadlocks.

So what does it means that Pony is deadlock free if it can implement deadlocking programs?

A better, more rigorous claim would be that the pony runtime is deadlock free or that there are no primitive blocking operations.

▲

perching_aix 4 days ago | parent [-]

Within the context of your Pony program you'll never be deadlocked. The virtual machine you implement capable of universal compute, and not enforcing this constraint, can be internally deadlocked, but this doesn't prevent your other Pony code from progressing necessarily - the deadlock is an internal state for that virtual machine, formally guaranteed to be confined to it.

I'd be hesitant to call this a "Pony runtime" property - to my understanding language runtimes just provide application bootstrapping and execution time standard library access. Pony code becomes machine code, managed by the OS as a process with some threads. This language property guarantees you that those threads will never "actually", "truly" deadlock. Code implemented on the Pony level can still progress if it chooses to do so, and Pony formally ensures it always has the option to choose so.

If your business requirements necessitate otherwise, that's a different matter, something you introduce and manage on your own.

▲

gpderetta 4 days ago | parent | next [-]

That's a bit like saying that pthreads is deadlock free because the Unix kernel can still schedule other programs. It is an useful guarantee, but it doesn't help fix my broken program.

	▲	perching_aix 4 days ago \| parent [-]
		Yes. If you want to encode soundness guarantees, you might want to look for a language with formal verification facilities instead, like Ada-SPARK. I'm not sure if there are any languages that allow you to pass down / inherit language constraints specifically, maybe Lisp or similar can do that? But then often that unfortunately wouldn't be actually helpful, as these requirements usually come from the outside (like in your Python example, it comes from Python being specified such that you can encode deadlocking logic in your Python code). For most everyone who aren't trying to implement the possibility of deadlocks in guestcode, this remains a useful property even without that.

▲

thayne 3 days ago | parent | prev [-]

You can absolutely have a pony program deadlock.

A simple example is if you get into a situation where two actors are both waiting for the other to send it a message.