For a more thorough approach: Would it be worth having something like we do for pointers, where we add an unknown_thread to the set (like we have unknown_pointer) but sill keep the threads that we have?

It would make Thread invalidation a bit more sensible by not just keeping the current one but adding something. Although it will make absolutely no difference (other than having to filter it out everywhere) if we don't properly and soundly handle unknown threads. Given that we don't properly handle unknown pointers anyway, it's probably not worth the effort now.

Also, it wouldn't save us from all the weird lattice hacks between Thread and Int, just like how it doesn't save Address from them.

Ugh, this doesn't even work for macOS because there pthread_t isn't an integer but some struct pointer. So we also need Address and Thread to join into a Thread...

Although it will make absolutely no difference (other than having to filter it out everywhere) if we don't properly and soundly handle unknown threads.

There are many cases where we actually do the sound thing (in creating all required threads) and as long as we are not overzealous about exploiting pthread_join(...) we are on the safe side.

Joining a thread id and and an int by ignoring the int means that when we call a pthread_join it looks as if we have a set of thread ids (or in the worst case a singleton), where in fact we incurred imprecision and our thread set does potentially not soundly describe all threads. In such a case, we should not exploit anything we learn through the pthread_join, because there are possibly other threads. But at this pthread_join there is no way of knowing if this issue occurred.

If we add this unknown_thread upon invalidation, we could warn on such a pthread_join (maybe it is indeed a bug), and offer an option how to proceed in such a case (as we do with unknown pointers).

There are many cases where we actually do the sound thing (in creating all required threads) and as long as we are not overzealous about exploiting pthread_join(...) we are on the safe side.

Not really, if we already have an unknown function pointer somehow, then spawning a thread from it will not spawn all the functions. Just like calling an unknown function pointer doesn't call all the functions.

If we add this unknown_thread upon invalidation, we could warn on such a pthread_join (maybe it is indeed a bug), and offer an option how to proceed in such a case (as we do with unknown pointers).

That only covers invalidation, but not any of the other cases Int and Thread might get joined (initialization, branched thread creation, joins inside partitioned arrays).

That only covers invalidation, but not any of the other cases Int and Thread might get joined (initialization, branched thread creation, joins inside partitioned arrays).

Why would the same logic not apply for all the other cases you listed?

Why would the same logic not apply for all the other cases you listed?

The solution you proposed was "add this unknown_thread upon invalidation". Or was it somehow unrelated?

Ah, sorry, I should have been more specific.
I meant "add this unknown_thread upon invalidation or incompatible join/widen/...".