Телеграмм чат группы rust_offtopic страница 17633

parrot.ru

Рейтинг популярных групп и каналов

В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

rust_offtopic

427 membersпожаловаться на группу

2020 August 24

r

red75prime in rust_offtopic

Constantine Drozdov

не думаю, что трансляцию из LLVM в команды CPU можно верифицировать, это решение эквивалентности программ

Невозможно доказать эквивалентность произвольных программ. Построить функцию, которая доказанно выдаёт на выходе семантически эквивалентный код должно быть возможно.

источник

22:07пожаловаться #1

CD

Constantine Drozdov in rust_offtopic

red75prime

Невозможно доказать эквивалентность произвольных программ. Построить функцию, которая доказанно выдаёт на выходе семантически эквивалентный код должно быть возможно.

Нас интересует не семантически эквивалентный код, а доказательство эквивалентности конкретного кода

источник

22:07пожаловаться #2

CD

Constantine Drozdov in rust_offtopic

например, x = 0 и xor eax, eax

источник

22:08пожаловаться #3

CD

Constantine Drozdov in rust_offtopic

mov eax, 0 нас не устраивает

источник

22:08пожаловаться #4

r

red75prime in rust_offtopic

Constantine Drozdov

Нас интересует не семантически эквивалентный код, а доказательство эквивалентности конкретного кода

Этот код получен определенным образом. Последовательным применением трансформаций, например. Можно доказать, что преобразование, удаляющее первую часть из последовательности операций вида x=1; x=2;, сохраняет семантику. Используем только такие доказанные преобразования. Получаем доказанно эквивалентную программу.

источник

22:16пожаловаться #5

CD

Constantine Drozdov in rust_offtopic

red75prime

Этот код получен определенным образом. Последовательным применением трансформаций, например. Можно доказать, что преобразование, удаляющее первую часть из последовательности операций вида x=1; x=2;, сохраняет семантику. Используем только такие доказанные преобразования. Получаем доказанно эквивалентную программу.

На нижнем уровне доказываем, что

        mov     rcx, QWORD PTR [rbp-8]
        movabs  rdx, 35958565445827586
        mov     rax, rcx
        imul    rdx
        mov     rsi, rcx
        sar     rsi, 63
        mov     rax, rdx
        sub     rax, rsi
        mov     rdx, rax
        sal     rdx, 9
        add     rdx, rax
        mov     rax, rcx
        sub     rax, rdx

эквивалент знакового деления i64 на 513

источник

22:18пожаловаться #6

r

red75prime in rust_offtopic

Было бы неплохо. Говорят ошибки в оптимизации деления компиляторами встречались довольно часто.

источник

22:30пожаловаться #7

2020 August 25

EG

Emmanuel Goldstein in rust_offtopic

Constantine Drozdov

На нижнем уровне доказываем, что

        mov     rcx, QWORD PTR [rbp-8]
        movabs  rdx, 35958565445827586
        mov     rax, rcx
        imul    rdx
        mov     rsi, rcx
        sar     rsi, 63
        mov     rax, rdx
        sub     rax, rsi
        mov     rdx, rax
        sal     rdx, 9
        add     rdx, rax
        mov     rax, rcx
        sub     rax, rdx

эквивалент знакового деления i64 на 513

Деление реально компилируется в такой треш?

источник

01:32пожаловаться #8

CD

Constantine Drozdov in rust_offtopic

Emmanuel Goldstein

Деление реально компилируется в такой треш?

Треш?

источник

01:32пожаловаться #9

EG

Emmanuel Goldstein in rust_offtopic

Была, вроде как, встроенная инструкция div для таких случаев

источник

01:33пожаловаться #10

EG

Emmanuel Goldstein in rust_offtopic

Это, правда, unsigned

источник

01:33пожаловаться #11

EG

Emmanuel Goldstein in rust_offtopic

Но есть idiv

источник

01:33пожаловаться #12

EG

Emmanuel Goldstein in rust_offtopic

И сложно поверить, что вот эта вот куча математических операций быстрее, чем одна инструкция

источник

01:33пожаловаться #13

EG

Emmanuel Goldstein in rust_offtopic

https://godbolt.org/z/jzf976
Реально не idiv, но и кода гораздо меньше

Compiler Explorer - Rust (rustc 1.45.2)

// Type your code here, or load an example.
pub fn div513(num: i64) -> i64 {
num / 513
}

источник

01:35пожаловаться #14

b

badtrousers in rust_offtopic

Emmanuel Goldstein

И сложно поверить, что вот эта вот куча математических операций быстрее, чем одна инструкция

ты просто не выкупаешь сложность этой инструкции

источник

01:39пожаловаться #15

b

badtrousers in rust_offtopic

div это очень дорого

источник

01:39пожаловаться #16

EG

Emmanuel Goldstein in rust_offtopic

Не настолько же.
И, как показывает godbolt, реальные компиляторы генерируют код вдвое короче этой портянки.

источник

01:40пожаловаться #17

b

badtrousers in rust_offtopic

тут согласен

источник

01:40пожаловаться #18

EG

Emmanuel Goldstein in rust_offtopic

А почему, собственно, в процессоре есть встроенные инструкции, которые дороже, чем их софтварная эмуляция? ELI5

источник

01:43пожаловаться #19

EG

Emmanuel Goldstein in rust_offtopic

Казалось бы, их можно было бы «хардварно» эмулировать на самом проце

источник

01:43пожаловаться #20