Pull to refresh
196
0
Михаил @mikhanoid

ИММ УрО РАН

Send message

Доказательство некорректности алгоритма сортировки Android, Java и Python

Reading time13 min
Views76K
Тим Петерс разработал гибридный алгоритм сортировки Timsort в 2002 году. Алгоритм представляет собой искусную комбинацию идей сортировки слиянием и сортировки вставками и заточен на эффективную работу с реальными данными. Впервые Timsort был разработан для Python, но затем Джошуа Блох (создатель коллекций Java, именно он, кстати, отметил, что большинство алгоритмов двоичного поиска содержит ошибку) портировал его на Java (методы java.util.Collections.sort и java.util.Arrays.sort). Сегодня Timsort является стандартным алгоритмом сортировки в Android SDK, Oracle JDK и OpenJDK. Учитывая популярность этих платформ, можно сделать вывод, что счёт компьютеров, облачных сервисов и мобильных устройств, использующих Timsort для сортировки, идёт на миллиарды.

Но вернёмся в 2015-й год. После того как мы успешно верифицировали Java-реализации сортировки подсчётом и поразрядной сортировки (J. Autom. Reasoning 53(2), 129-139) нашим инструментом формальной верификации под названием KeY, мы искали новый объект для изучения. Timsort казался подходящей кандидатурой, потому что он довольно сложный и широко используется. К сожалению, мы не смогли доказать его корректность. Причина этого при детальном рассмотрении оказалась проста: в реализации Timsort есть баг. Наши теоретические исследования указали нам, где искать ошибку (любопытно, что ошибка была уже в питоновской реализации). В данной статье рассказывается, как мы этого добились.

Статья с более полным анализом, а также несколько тестовых программ доступны на нашем сайте.
Читать дальше →

Построение графиков в LaTeX/PGFPlots

Reading time13 min
Views104K
image

Данная статья посвящена описанию работы с пакетом PGFPlots, разработанного для популярной настольной издательской системы LaTeX. Однако, если вы даже не знакомы с последней, это не повод расстраиваться и бросать чтение этой статьи, ведь, возможно, те замечательные примеры, которые будут далее приведены, и необычайная мощность и удобство PGFPlots вдохновят вас на изучение LaTeX.
Читать дальше →

JIT-компилятор как учебный проект в Академическом Университете

Reading time10 min
Views29K
Около шестнадцати лет назад вышла первая версия Hotspot – реализация JVM, впоследствии ставшая стандартной виртуальной машиной, поставляемой в комплекте JRE от Sun.

Основным отличием этой реализации стал JIT-компилятор, благодаря которому заявления про медленную Джаву во-многих случаях стали совсем несостоятельными.
Сейчас почти все интерпретируемые платформы, такие как CLR, Python, Ruby, Perl, и даже замечательный язык программирования R, обзавелись своими реализациями JIT-трансляторов.

В рамках этой статьи я не планирую проливать свет на малоизвестные детали реализации промышленных JIT-компиляторов, скорее это будет совсем поверхностное ознакомление с азами и рассказ про учебный проект по соответствующей тематике.

Таким образом вам может быть интересно под катом, если:
  • Вы принципиально не понимаете, что такое JIT-компилятор, или у вас есть легкое непонимание, чем такой подход существенно лучше интерпретации.
  • Вы хотели бы написать простой JIT для своего интерпретируемого языка.
  • Вы преподаете курс «Языки программирования и компиляторы», и не против сделать практическое задание для студентов еще интересней.
  • Вам интересно, как нарисована эта картинка.


Читать дальше

Как работает мозг?

Reading time8 min
Views120K
Этот пост написан по мотивам лекции Джеймса Смита, профессора Висконсинского университета в Мадисоне, специализирующегося в микроэлектронике и архитектуре вычислительных машин.

История компьютерных наук в целом сводится к тому, что учёные пытаются понять, как работает человеческий мозг, и воссоздать нечто аналогичное по своим возможностям. Как именно учёные его исследуют? Представим, что в XXI веке на Землю прилетают инопланетяне, никогда не видевшие привычных нам компьютеров, и пытаются исследовать устройство такого компьютера. Скорее всего, они начнут с измерения напряжений на проводниках, и обнаружат, что данные передаются в двоичном виде: точное значение напряжения не важно, важно только его наличие либо отсутствие. Затем, возможно, они поймут, что все электронные схемы составлены из одинаковых «логических вентилей», у которых есть вход и выход, и сигнал внутри схемы всегда передаётся в одном направлении. Если инопланетяне достаточно сообразительные, то они смогут разобраться, как работают комбинационные схемы — одних их достаточно, чтобы построить сравнительно сложные вычислительные устройства. Может быть, инопланетяне разгадают роль тактового сигнала и обратной связи; но вряд ли они смогут, изучая современный процессор, распознать в нём фон-неймановскую архитектуру с общей памятью, счётчиком команд, набором регистров и т.п. Дело в том, что по итогам сорока лет погони за производительностью в процессорах появилась целая иерархия «памятей» с хитроумными протоколами синхронизации между ними; несколько параллельных конвейеров, снабжённых предсказателями переходов, так что понятие «счётчика команд» фактически теряет смысл; с каждой командой связано собственное содержимое регистров, и т.д. Для реализации микропроцессора достаточно нескольких тысяч транзисторов; чтобы его производительность достигла привычного нам уровня, требуются сотни миллионов. Смысл этого примера в том, что для ответа на вопрос «как работает компьютер?» не нужно разбираться в работе сотен миллионов транзисторов: они лишь заслоняют собой простую идею, лежащую в основе архитектуры наших ЭВМ.

Моделирование нейронов


Кора человеческого мозга состоит из порядка ста миллиардов нейронов. Исторически сложилось так, что учёные, исследующие работу мозга, пытались охватить своей теорией всю эту колоссальную конструкцию. Строение мозга описано иерархически: кора состоит из долей, доли — из «гиперколонок», те — из «миниколонок»… Миниколонка состоит из примерно сотни отдельных нейронов.



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

Очень быстрые классы на JavaScript с красивым синтаксисом

Reading time8 min
Views54K
При написании серьезных проектов перед JavaScript программистами встает выбор: пожертвовать качеством кода и писать классы руками, или же пожертвовать скоростью и использовать систему классов. А если использовать систему, то какую выбрать?

В статье рассмотрена система автора, которая не уступает по скорости классам, написанным «от руки» (другими словами — одна из самых быстрых в мире). Но при этом классы имеют приятную структуру в стиле Си.

Системы классов


Есть шутка, что каждый программист должен написать свою систему классов. Кто не знаком с проблемой — смотрите этот комментарий, там их собрано минимум 50 штук.

Каждый из этих велосипедов отличается своим набором возможностей, своим стилем программирования и своим падением скорости. Так, например, создание класса MooTools примерно в 90 раз медленнее, чем создание класса, написанного от руки. Зачем тогда нужны все эти системы?
Читать дальше →

Skyforge: технологии рендеринга

Reading time16 min
Views104K


Всем привет! Меня зовут Сергей Макеев, и я технический директор в проекте Skyforge в команде Allods Team, игровой студии Mail.Ru Group. Мне хотелось бы рассказать про технологии рендеринга, которые мы используем для создания графики в Skyforge. Расскажу немного о задачах, которые стояли перед нами при разработке Skyforge с точки зрения программиста. У нас свой собственный движок. Разрабатывать свою технологию дорого и сложно, но дело в том, что на момент запуска игры (три года назад) не было технологии, которая могла бы удовлетворить всем нашим запросам. И нам пришлось самим создать движок с нуля.
Читать дальше →

Категории Клейсли

Reading time9 min
Views27K

Композиция логирования


Вы видели, как сделать категорию типов и чистых функций. Я также упомянул, что есть способ смоделировать побочные эффекты, или нечистые функции, в рамках теории категорий. Давайте рассмотрим пример: функции, которые логируют или записывают ход своего выполнения.
Читать дальше →

Ансамбль синапсов – структурная единица нейронной сети

Reading time11 min
Views36K


В мае прошлого года сотрудники лаборатории глубокого обучения Гугла и учёные из двух американских университетов опубликовали исследование «Intriguing properties of neural networks». Статья о нём вольно пересказывалась здесь на Хабре, и само исследование также критиковалось специалистом из ABBYY.

Гугловцы в результате своих исследований разочаровались в способностях нейронов сети распутывать признаки входных данных и стали склоняться к мысли, что нейронные сети не распутывают семантически значимые признаки по отдельным структурным элементам, а хранят их во всей сети в целом как в голограмме. В нижней части иллюстрации к этой статье чёрно-белыми я привёл карты активации 29, 31 и 33-его нейронов сети, которую обучил рисовать картинку. То, что тушка птицы без головы и крыльев, изображаемая для примера 29-ым нейроном, покажется людям семантически значимым признаком гугловцы считают всего лишь ошибкой интерпретации наблюдателя.

В статье я на реальном примере постараюсь показать, что и в искусственных нейронных сетях распутанные признаки можно обнаружить. Постараюсь объяснить, почему гугловцы увидели то, что они увидели, а распутанных признаков увидеть не смогли, и покажу, где в сети скрываются семантически значимые признаки. Статья является популярной версией доклада, прочитанного на конференции «Нейроинформатика — 2015» в январе этого года. Наукообразную версию статьи можно будет почитать в материалах конференции.
Очень-очень много трафика

Новые оптимизации для х86 в GCC 5.0: PIC в 32-битном режиме

Reading time3 min
Views8.4K
Данный пост продолжает серию из трех статей об оптимизациях для x86 в GCC 5.0. В предыдущей статье речь шла о векторизации. Напомню, что GCC 5.0 находится сейчас в фазе stage3, то есть внедрение новых оптимизаций уже фактически заверешено и уровень производительности за редким исключением останется прежним и в продуктовом релизе. Сегодня речь пойдет об ускорениях позиционно-независимого кода или position independent code (PIC) в 32-битном режиме для x86.
Читать дальше →

Padding Oracle Attack или почему криптография пугает

Reading time7 min
Views70K
Все мы знаем, что не следует самостоятельно реализовывать криптографические примитивы. Мы также в курсе, что даже если мы хитрым образом развернем порядок букв во всех словах сообщения, сдвинем каждую букву по алфавиту на 5 позиций и разбавим текст случайными фразами, чтобы сбить атакующих с пути, наш замечательный шифр скорее всего вскроет любой мало-мальски знакомый с криптографией человек (а в данном случае с задачей справится и в меру умный 12-летний подросток).

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

Мой посыл не в том, что убедить вас отказаться от самостоятельного использования криптографических средств или пойти и нанять консультанта с зарплатой от $1000 в час всякий раз когда вы задумываетесь о шифровании.
Частично я веду к тому, что вам никогда не следует расслабляться, всегда нужно быть начеку, изыскивая пути, которые злоумышленник может использовать для получения дополнительной информации о вашей системе, а частично к тому, что Padding Oracle Attack является крутой демонстрацией всего этого. Итак, начнем.
Читать дальше →

SageMathCloud — мечта для любителей Python, математики и Linux

Reading time7 min
Views38K
SageMathCloud (сокращённо SMC) — это онлайновый сервис, в котором можно написать математический или любой другой расчёт в Sage или IPython Notebook. Расчёт можно комбинировать с HTML, CSS, JavaScript, CoffeeScript, Go, Fortran, Julia, Gap, Axiom, R, Ruby, Perl, Maxima, Maple, Markdown, Wiki (и это неполный список!). При редактировании поддерживается мультикурсорность, можно включить биндинги Vim или Sublime Text. Пользователю также доступна консоль Ubuntu и доступ к проекту по ssh. Можно создавать документы LaTeX и встраивать в них код на Python, который не будет отображаться в итоговом pdf. Широкие возможности позволяют написать не просто расчёт с 2D и 3D графикой, а целое интерактивное приложение или собственный веб-сервер на Flask. Можно расшарить расчёт пользователям на редактирование, и Вы будете видеть, что они меняют и даже где стоит их курсор! При этом великолепии SageMathCloud имеет открытый исходный код, который выложен на Github.



Читать дальше →

ODROID-C1 — обзор и сравнение с RPi

Reading time4 min
Views107K

Доброго времени суток, уважаемые хабровчане и просто случайные гости.
В данном посте я сделал небольшой обзор нового мини-компьютера ODROID-C1 в сравнении с Raspberry Pi при использовании обоих устройств в качестве ТВ-приставки/медиасервера для дома. Статья рассчитана на знатоков Raspberry Pi или других похожих платформ.
Читать дальше →

Руководство хакера по нейронным сетям. Глава 2: Машинное обучение. Обучение сети на основе метода опорных векторов (SVM)

Reading time8 min
Views15K
Содержание:
Глава 1: Схемы реальных значений
Часть 1:
   Введение   
      Базовый сценарий: Простой логический элемент в схеме
      Цель
         Стратегия №1: Произвольный локальный поиск

Часть 2:
         Стратегия №2: Числовой градиент

Часть 3:
         Стратегия №3: Аналитический градиент

Часть 4:
      Схемы с несколькими логическими элементами
         Обратное распространение ошибки

Часть 5:
         Шаблоны в «обратном» потоке 
      Пример "Один нейрон"

Часть 6:
      Становимся мастером обратного распространения ошибки


Глава 2: Машинное обучение
Часть 7:
      Бинарная классификация

Часть 8:
      Обучение сети на основе метода опорных векторов (SVM)

Часть 9:
      Обобщаем SVM до нейронной сети

Часть 10:
      Более традиционный подход: Функции потерь



В качестве конкретного примера давайте рассмотрим SVM. SVM – это очень популярный линейный классификатор. Его функциональная форма имеет именно такой же вид, как я описывал в предыдущем разделе — f(x,y)=ax+by+c. На данном этапе, если вы видели описание SVM, вы наверняка ожидаете, что я буду определять функцию потерь SVM и погружаться в пояснения свободных переменных, геометрических понятий больших полей, ядер, двойственности и пр. Но здесь я бы хотел воспользоваться другим подходом.
Читать дальше →

ODROID-C1 — форма от Raspberry Pi B+, 4 ядра по 1500MHz, 1GB и цена $35

Reading time2 min
Views37K
Корейские ребята из компании Жёсткоеядрышко (Hardkernel) выпустили в жизнь свой новый микрокомпьютер ODROID-C1, который сделан по подобию Raspberry Pi B+ в том же формфакторе и с тем же разъёмом GPIO. При этом, он обладает четырёхядерным процессором Cortex-A5 с частотой 1,5GHz, 1GB DDR3, гигабитной сетевой картой и прочими прелестями, которые заметно превосходят возможности малинки.

image

Немного предыстории


Ещё до этого Hardkernel выпустила ODROID-W, который имел тот же процессор от Broadcom, что и малинка, был программно совместим, а главным отличием были значительно меньшие размеры платы, особенно в высоту. Но ребятам, которые пекут малиновые пироги, это не понравилось и Broadcom запретила продавать Hardkernel свои процессоры. Была выпущена только одна партия ODROID-W. Её анонсировали в июле, а уже в сентябре появилось сообщение об отказе Broadcom в поставках.

Теперь же, Raspberry Pi B+ получил серьёзного конкурента, и хотя корейский вариант и менее известен, но он хорошо подходит тем, кому, как минимум, нужно больше производительности.

Сравнение и подробности

Итальянские ученые опубликовали самые подробные фотографии нервных окончаний

Reading time1 min
Views12K


То, что вы видите на анонсной фотографии — вовсе не творение очередного художника-асбтракциониста, который отобразил собственные ассоциативные фантазии на холсте. Это — фотография нервных окончаний обычных мышей, полученные путем использования специальной техологии.

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

Читать дальше →

Многозадачность в ядре Linux: прерывания и tasklet’ы

Reading time6 min
Views77K
Котейка и младшие братьяВ предыдущей своей статье я затронула тему многопоточности. В ней речь шла о базовых понятиях: о типах многозадачности, планировщике, стратегиях планирования, машине состояний потока и прочем.

На этот раз я хочу подойти к вопросу планирования с другой стороны. А именно, теперь я постараюсь рассказать про планирование не потоков, а их “младших братьев”. Так как статья получилась довольно объемной, в последний момент я решила разбить ее на несколько частей:
  1. Многозадачность в ядре Linux: прерывания и tasklet’ы
  2. Многозадачность в ядре Linux: workqueue
  3. Protothread и кооперативная многозадачность

В третьей части я также попробую сравнить все эти, на первый взгляд, разные сущности и извлечь какие-нибудь полезные идеи. А через некоторое время я расскажу про то, как нам удалось применить эти идеи на практике в проекте Embox, и про то, как мы запускали на маленькой платке нашу ОС с почти полноценной многозадачностью.

Рассказывать я постараюсь подробно, описывая основное API и иногда углубляясь в особенности реализации, особо заостряя внимание на задаче планирования.
Читать дальше →

Псевдопрактический пример замыканий и декораторов

Reading time4 min
Views17K
Когда я только начинал изучать Python, большое впечатление на меня произвели route-декораторы в известном фреймворке flask. Конечно, я догадывался, как они могли быть реализованы, но как всегда желание писать (а не читать) превзошло необходимость взглянуть на исходный код flask, и мне пришлось выдумать то, что могло бы выглядеть так же лапидарно, как вышеупомянутые декораторы из flask'а. Упражнение на тему замыканий, декораторов и области видимости в Python могло бы выглядеть так:

def do_something(p):
    return p

@implements(do_something, lambda: not p % 2)
def do_mod2_something(p):
    return p / 2

@implements(do_something, lambda: not p % 3)
def do_mod3_something(p):
    return p / 3

do_something(10)  # returns 5
do_something(9)   # returns 3
do_something(11)  # returns 11


Как реализовать декоратор @implements? Может ли подобная реализация использоваться где-то в реальных проектах — вопрос, который мы редко принимаем во внимание, выдумывая себе упражнения для понимания того, как работают те или иные программы. Мне показалось, что это выглядит как некое замещение (override) функции, имеющее место в других языках программирования.
Читать дальше →

Графен: тончайшая твердая смазка

Reading time5 min
Views51K
Обычно, когда заходит речь о графене, сразу возникают ассоциации с чем-то микроскопическим, невидимым невооруженным взглядом, и, пока что, не имеющим какого-либо практического применения за пределами лабораторий. Такое впечатление усиливается после прочтения новостей о последних «прикладных» открытиях — будь то «самый тонкий двигатель», или «самый тонкий и гибкий транзистор». Однако, помимо таких хоть и полезных, но (пока) далеких от реальной жизни применений, есть области, где графен может применяться прямо сейчас, причем в макроскопическом масштабе. Одна из них — трибология.
Читать дальше

На взрыволёте к Юпитеру

Reading time8 min
Views210K

Ограниченность химических ракет была ясна ещё до начала регулярных космических пусков. Формула Циолковского прямо говорит, что на привычных нам двигателях можно слетать на Луну (стартуя на ракете тысячи в три тонн начальной массы и вернувшись в кораблике в несколько тонн), с огромным трудом долететь до Марса (с во много раз худшим соотношением начальной/конечной массы), но вот покорить Солнечную систему на химических ракетах нельзя. Поэтому уже в середине двадцатого века стали появляться альтернативные проекты, наиболее ярким из которых стал атомный взрыволёт (импульсная ракета). В этом посте мы поговорим о его конструкции, истории создания, перспективах в 21 веке, а ещё слетаем на нём к Юпитеру в Orbiter'е.
Читать дальше →

Information

Rating
Does not participate
Registered
Activity

Specialization

System Software Engineer, scientific programming
Scheme
C
Assembler
Linux
Maths
Julia
Compilers
Math modeling
Machine learning
Computer Science