В компилируемых языках часто случается такое, что компилятор делает какой-то выбор за программиста. Например, как расположить локальные переменные на стеке, в каком порядке вызвать чистые функции, и так далее. В идеале эти выборы были бы неразличимы с точки зрения программы и выступали чисто незаметной оптимизацией, но на практике это не так — например, я могу вывести адрес локальной переменной и так узнать, куда конкретно на стек её решил положить компилятор:
fn f() {
int x, y;
printf("%p %p", &x, &y);
}
Так мы встречаемся с недетерминированным поведением: компилятор делает выбор, который приводит к более простому с его точки зрения коду, а на наши плечи ложится задача написать такую программу, которая работает корректно независимо от выбора компилятора.
Ещё есть такая штука, как UB. Основная идея UB в том, что если компилятор имеет право сделать какое-то предположение, а оно оказывается неверно, то принципу взрыва делать дальше что-либо полезное и предсказуемое становится невозможно. На UB надо смотреть как на противоречие в системе аксиом.
Что происходит, когда недетерминизм встречается с UB? Например, в программе if ((char)(&x) % 3 == 0) __builtin_unreachable(); UB случается или не случается в зависимости от выбора адреса x. Поскольку мы как программисты обязаны написать код, который работает при любом выборе компилятора, компилятор на это может полагаться и предполагать, что UB не случается никогда, и выбрать любую ветку — в частности ту, которая приводит к UB. Противоречие. Следовательно, программа содержит UB.
Это так называемый демонический недетерминизм: компилятор имеет право сделать любой выбор, и поэтому поведение программы определено только тогда, когда оно определено для всех возможных выборов. Это самый популярный сценарий, и с ним мы встречаемся, например, в примитивах типа freeze, в оптимизациях malloc до локальных аллокаций, и так далее.
Но бывает ещё другой недетерминизм. Если вы кастуете два указателя к uintptr_t, делаете с ними непонятную магию, а потом кастуете обратно, компилятор должен решить, какой провенанс присвоить получившемуся указателю. C и Rust гарантируют, что с (int*)(uintptr_t)p можно работать так же, как с p, поэтому здесь выбор должен быть не в пользу компилятора, а в пользу программиста — если существует провенанс, при котором поведение программы корректно, выбран должен быть именно он. Это ангельский недетерминизм.
На демонический и ангельский недетерминизм можно смотреть как на кванторы "для любого" и "существует". Программа bool b = demonic(); ... корректна, если для любого b программа ... корректна; программа bool b = angelic(); ... корректна, если существует такой b, что программа ... корректна.
Естественно, возникает вопрос: что происходит, когда эти кванторы сочетаются? Поскольку из ∀x. ∃y. P(x, y) не следует ∃y. ∀x. P(x, y), переставлять demonic() и angelic() в общем случае некорректно. Например, программа
if demonic() == angelic() { core::hint::assume_unreachable(); }
...не содержит UB, а
if angelic() == demonic() { core::hint::assume_unreachable(); }
...содержит. Но это должно означать, что такие простые операции, как касты и аллокации локальных переменных, не могут быть чистыми. Естественно, подписываться на такое никто не хочет, потому что перф и бла-бла-бла. Поэтому что-то отсюда нужно формализовывать иначе, но что и как — никто не знает.
Читать ещё:
https://github.com/rust-lang/unsafe-code-guidelines/issues/392
https://rust-lang.zulipchat.com/#narrow/channel/136281-t-opsem/topic/Resource.20request.3A.20quantifier.20ordering.20in.20PLT/with/296767256
https://rust-lang.zulipchat.com/#narrow/channel/136281-t-opsem/topic/Formalizing.20angelic.20and.20demonic.20choice/with/296355551
fn f() {
int x, y;
printf("%p %p", &x, &y);
}
Так мы встречаемся с недетерминированным поведением: компилятор делает выбор, который приводит к более простому с его точки зрения коду, а на наши плечи ложится задача написать такую программу, которая работает корректно независимо от выбора компилятора.
Ещё есть такая штука, как UB. Основная идея UB в том, что если компилятор имеет право сделать какое-то предположение, а оно оказывается неверно, то принципу взрыва делать дальше что-либо полезное и предсказуемое становится невозможно. На UB надо смотреть как на противоречие в системе аксиом.
Что происходит, когда недетерминизм встречается с UB? Например, в программе if ((char)(&x) % 3 == 0) __builtin_unreachable(); UB случается или не случается в зависимости от выбора адреса x. Поскольку мы как программисты обязаны написать код, который работает при любом выборе компилятора, компилятор на это может полагаться и предполагать, что UB не случается никогда, и выбрать любую ветку — в частности ту, которая приводит к UB. Противоречие. Следовательно, программа содержит UB.
Это так называемый демонический недетерминизм: компилятор имеет право сделать любой выбор, и поэтому поведение программы определено только тогда, когда оно определено для всех возможных выборов. Это самый популярный сценарий, и с ним мы встречаемся, например, в примитивах типа freeze, в оптимизациях malloc до локальных аллокаций, и так далее.
Но бывает ещё другой недетерминизм. Если вы кастуете два указателя к uintptr_t, делаете с ними непонятную магию, а потом кастуете обратно, компилятор должен решить, какой провенанс присвоить получившемуся указателю. C и Rust гарантируют, что с (int*)(uintptr_t)p можно работать так же, как с p, поэтому здесь выбор должен быть не в пользу компилятора, а в пользу программиста — если существует провенанс, при котором поведение программы корректно, выбран должен быть именно он. Это ангельский недетерминизм.
На демонический и ангельский недетерминизм можно смотреть как на кванторы "для любого" и "существует". Программа bool b = demonic(); ... корректна, если для любого b программа ... корректна; программа bool b = angelic(); ... корректна, если существует такой b, что программа ... корректна.
Естественно, возникает вопрос: что происходит, когда эти кванторы сочетаются? Поскольку из ∀x. ∃y. P(x, y) не следует ∃y. ∀x. P(x, y), переставлять demonic() и angelic() в общем случае некорректно. Например, программа
if demonic() == angelic() { core::hint::assume_unreachable(); }
...не содержит UB, а
if angelic() == demonic() { core::hint::assume_unreachable(); }
...содержит. Но это должно означать, что такие простые операции, как касты и аллокации локальных переменных, не могут быть чистыми. Естественно, подписываться на такое никто не хочет, потому что перф и бла-бла-бла. Поэтому что-то отсюда нужно формализовывать иначе, но что и как — никто не знает.
Читать ещё:
https://github.com/rust-lang/unsafe-code-guidelines/issues/392
https://rust-lang.zulipchat.com/#narrow/channel/136281-t-opsem/topic/Resource.20request.3A.20quantifier.20ordering.20in.20PLT/with/296767256
https://rust-lang.zulipchat.com/#narrow/channel/136281-t-opsem/topic/Formalizing.20angelic.20and.20demonic.20choice/with/296355551