Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2021-03-26 09:06:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: sick
Музыка:Cawatana - ADVOCATION FOR PRIVILEGES
Entry tags:boloto, pop, putin, smeshnoe

два кремлевских защекана
Из жизни путинских проституток.

1. Моргенштерна оштрафовали за незаконное использование

песни "Владимир Путин - молодец". С рэпера взыскали 300
тыс. рублей.

Рэп это кал, конечно, но русский рэп это особенный кал,
он даже на бристольскую шкалу не укладывается.

2. Откровенная беседа Олега Кашина и Марии Бароновой.

Требуют расстрелять Навального как бешеную собаку
репрессий против организаторов незаконных митингов.

О. Кашин:


- У нас полиция качественная и цензура качественная. Но
все-таки даже конкретные ноги конкретным людям
ломали. Помнишь этого парня, который бегал перед мэрией
в 2019 году, ему буквально сломали ногу. И девушку,
которую в живот ударили. Полицейского искали. Это мягче,
чем в Америке, мягче, чем в Белоруссии. Слава богу,
слава Владимиру Путину.

М. Баронова:

- Им не будет ломать ногу полицейский. Ты отлично знаешь,
что с обеих сторон наши митинги сильно отличаются от
майданов и от Белоруссии. У нас невероятно качественно
работает полиция.

О. Кашин:

-- Мы с тобой - два кремлевских защекана.

По ссылке отсюда:
https://potsreotizm-new.livejournal.com/7316718.html

Кстати, оба кремлевских защекана, помимо активного
крымнашизма, патриотизма и запутинщины, имели прекрасную
карьеру в белоленточных организациях "оппозиции".
Мне кажется, этого уже достаточно, чтобы поставить
на болотной оппозиции жирный крест. Пока таких
персонажей выбирают в "Координационный совет оппозиции"
вместо того, чтобы выкидывать из дома пинками,
никакой "оппозиции" у вас не будет.

Привет



(Читать комментарии) - (Добавить комментарий)


[info]stereo_sanctity
2021-03-27 20:04 (ссылка)
а что не так с верификацией ПО ? новое железо уже как бы лет 10 без тонны работ по доказательствам не пилится

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2021-03-27 20:22 (ссылка)
ну речь же про ПО, а не про железо

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]stereo_sanctity
2021-03-27 22:25 (ссылка)
так в железе куча ПО зашита

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2021-03-27 23:53 (ссылка)
то для чего model checking используют - это не совсем ПО, на мой взгляд.
слишком отдельная ниша, хотя можно поспорить
туда же sat-рилейтед штуки для процов.
z3 вроде для драйверов использовали экспериментально, но тоже такое себе ПО

если говорить про мейнстрим верификации типа coq, то там достаточно грустно всё, экстракторы неверефицированные стоят, даже ихний compcert не то чтобы особенно взлетел, особенно с учетом уровня людей и вложенных усилий, хотя щас уже хз что там происходит
(см https://thedeemon.livejournal.com/120510.html)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]stereo_sanctity
2021-03-28 01:17 (ссылка)
Replacing Testing with Formal Verification in Int... Processor Execution Engine Validation

Formal verification of arithmetic datapaths has been part of the estab-lished methodology for most Intel processor designs over the last years, usually in the role of supplementing more traditional coverage oriented testing activities. For the recent Int... design we took a step further and used formal verification as the primary validation vehicle for the core execution cluster...

я про вот эту штуку
это ай-семь, 2009 год, сейчас все архитектуры новые уже такого труда требуют, например: https://github.com/SymbioticEDA/riscv-formal

> compcert
ну это все-таки странная история изначально, учитывая насколько Си большая пофакту штука, это сделать все же сложнее чем для ассемблера, особенно на компиляторы Си на разных архитектурах ассемблера. насколько я понимаю софт, это куда сложнее чем переписать линукс с нуля например. но Think Big! принцип хороший, так что все правильно делают, просто изначально понятно было что настолько много чуваков со свободным временем под свою движуху не найдут
сейчас, кстати, есть похожая движуха, чуваки верифицируют части раста или там нима, иногда баги фиксят; так что оно конечно вцелом полезно, но много менее полезно чем для железа

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2021-03-28 12:58 (ссылка)
ну дык это чисто разработка железа, ну да, Харрисон там ебашит
sat-солверы и всё такое, схемы процессоров проверяют.
но это не про ПО совсем.

(Ответить) (Уровень выше)


(Читать комментарии) -