Below are the 20 most recent journal entries recorded in avlasov's LiveJournal:

[ << Previous 20 ]

Monday, May 21st, 2012
7:03 pm	Паштет из рябчиков* *с добавлением конины состав: конина (100%) (Comment on this)
Saturday, May 19th, 2012
1:55 am	Shared Memory GC Хочу еще раз подчеркнуть одну мысль. Есть такой распространенный миф, которому я и сам был подвержен длительное время, что весьма трудно написать GC в случае параллельного мутатора, т.е. когда потоки одновременно лазиют в общую память. Я условно называю сей класс коллекторов Shared Memory GC, т.е. GC который умеет собирать мусор в shared memory. На самом деле, сосбственно GC не есть проблема. Вобщем-то алгоритмы GC достаточно просты. Но суровые трудности все равно есть. Просто хороший производительный GC требует определенной поддержки от кодогенератора, ну и от рантайма. Да вообще говоря и от языка. А вот соблюсти все эти условия крайне тяжело, особенно в какой-то общей библиотеке или библиотеках. На данный момент, я так понимаю эта проблема в общем виде не решена. Но это не значит, что в данном конкретном случае нельзя сделать shmem сборку мусора. Например можно сделать тупой и медленный GC с помощью референс каунтинг, используя атомарные инкременты на каждый чих. COM так делает и не жужжит. Как я писал ранее, можно сделать консервативный коллектор, например использовать libgc. Тоже не проблема. Ну будет он часть мусора пропускать, да и хрен с ним. Ну компактить не будет, потормознее будет, выделение памяти медленное. Для многих задач, это не будет проблемой. По крайней мере, от использования многопоточности можно ожидать больше ускорения, нежели издержек консервативного GC. Хотя для определенных языков типа функциональных это будет хреново, они выделяют много объектов, так что для них generational GC весьма важен. В то же время, они не так часто память мутируют. Т.е. для функ языков можно сделать свои shmem коллекторы, также относительно не сложно. А вот (mostly)exact GC требует поддержки компилятора. Хотя это можно сделать весьма просто - тупо держать root ссылки на стэке или в куче. Ну или пометить их тэгами. Ну типа shadow стэк. Будет медленно. Но например для интерпретаторов совершенно не проблема. Посему непонятно, почему для Питона до сих пор нет многопоточного интерпретатора. Он кагбэ совершенно не страдает, от того что интерпретация работает медленнее компилируемого кода. А в случае интерпретатора выдавать список root'овых объектов совершенно не проблема. Действительно серьезной проблемой является кодогенератор, который бы генерил нужную информацию для GC. Собственно, эта проблема тоже не так страшна - относительно задачи написания качественного кодогенератора. Но большинство народу все-таки предпочитает юзать существующие кодогенераторы, ну и мало кто имеет квалификацию, чтобы доработать кодогенератор, чтобы он выдавал нужную для GC инфу. Точнее, поскольку для кодогенератора выходят новые версии, то их кагбэ тоже надо будет дорабатывать. Опять-таки отмечу, что есть простые способы обойти эти проблемы, использую сторонний кодогенератор, просто это будет работать медленнее, нежели доработать сей кодогенератор. Есть еще интересный класс GC, на основе read barrier'ов. Они обычно считаются очень медленными, ибо read'ы сильно превалируют над write'ами, особенно в функ языках. Но реальные реализации, выглядят интересными, ибо используют различные оптимизации для снижения издержек. У меня на данный момент есть идея соединить в едином порыве три вида управления памятью (два из них GC): 1 локальный GC, независимо от остальных потоков, т.е. без stop the world - реализована в Manticore и вроде как в недавном Хаскеле. Требует эакуации шаред объектов - что хорошо согласуется с гибридной актор/неакторской моделью 2 глобальный GC - моя идея реализовать конкруетнтый GC на read-barrier'ах, который (почти) не будет стопать ворлд 3 а также заюзать region'ы - это имеет ряд бенефитов и для GC. также хорошо вписывается в гибридный акторский модель (2 Comments |Comment on this)
12:19 am	Управление памятью для гибридной актор/неакторской многопоточности. Часть 2 Собсно, для чего требуется гибридная акторско/неакторская система? Писать многопоточность сильно проще для акторов. Однако, если акторы взаимодействуют через БД/кэш, то БД/кэш лучше писать многопоточным, потому как запросы в такую систему высококонкурентны, и их не всегда можно изолировать друг от друга. Иными словами, если мы конструируем систему в акторском стиле, интенсивный конкурентный доступ к определенной информации, которые так или иначе, а все равно обычно есть, вытесняется в акторов специального вида, обычно БД и/или кэш. Часто таких "акторов" выносят в отдельный процесс, обычно на другом компьютере. Однако, сие имеет существенные издержки (сериализация/десериализация, пересечение границы процесса, передача по сети). Вообще говоря, скорее большие, чем маленькие. Конечно, точные цыфры зависят от системы, но потенциально - вплоть до снижения издержек на порядок. Реализовать гибридную систему в рамках одного процесса можно двумя способами. Первый - реализовать акторов в рамках shmem системы, как это обычно делается в JVM/CLR. Т.е. ограничить обычные потоки, до уровня акторов, так или иначе не давая им взаимодействовать через shmem непосредственно. У сего способа есть один существенный недостаток: поскольку акторы с точки зрения рантайма все-таки потенциально могут лазить в shmem (а в специальных точках они так и делают), то и обращаться с ними надо как с таковыми. Иными словами, строго изолировать их от других процессов потоков. А значит надо их останавливать для (глобальной) сборки мусора. Т.е. любой поток в системе, может быть остановлен, хотя может реально это и не есть столь необходимо. NB Вообще в CLR есть специальный механизм для разделения прилад - appartment'ы вроде называются, а также там отдельно водятся не-managed потоки. Не в курсе, можно ли у них отдельно GC политики варьировать. В Жабе вобщем-то тоже можно нативные потоки параллельно жабьим гонять. Есть однако второй вариант реализации гибридной акторско/неакторской модели: в рамках одного процесса, ввести разные политики гарбидж коллекци для разных потоков. Естественно, обмен информации между доменами с разными политиками будет сопровождаться дополнительными действиями, чтобы выполнялись инварианты. Но обычно по любому выполняется копирование, так что это не страшно. К тому же возможны дополнительные оптимизации. Поскольку акторы обычно будут выполняться в однопоточном контексте (ибо их так гораздо проще программировать), то и политики GC для них будут гораздо проще, и эффективнее. Т.е. не надо заботится о синхронизации, не надо останавливать все треды, нет нужды инструментировать/патчить код. Собственно, как я писал ранее, во многих случаях можно вообще не делать GC - если запросы выполняются в ограниченное время, то всю использованную память можно освободить после окончания запроса. А "эвакуапция" выживших объектов будет вполне естественно выполнятся при сохраненнии состояния в специализированные "персистенс" акторы, типа БД/кэш. (2 Comments |Comment on this)
Friday, May 18th, 2012
10:31 pm	Управление памятью для гибридной актор/неакторской многопоточности Программирование многопоточности можно разделить на две категории: с shared memory и с передачей сообщений. Последний вариант условно называем актор-стайл, ибо акторы могут взаимодействовать лишь обменом сообщений. Разумеется возможны промежуточные варианты. Типа существование акторов одновременно с потоками, мутирующими общую память в рамках одного процесса. Либо многопоточные внутри себя акторы. Вот гибридный вариант меня и интересует в данном случае. Как я писал ранее, создание "хорошего" гарбдж коллектора в случае shared-memory модели, задача весьма нетривиальная. Поэтому многие разработчики языков либо тупо ставят GIL (Python/Ruby), либо реализуют акторскую многопоточность, как к примеру в Erlang'е и Go. Реальные shared memory коллекторы тоже есть: JVM и CLR. А также Хаскелл - но в Хаскелле, как в чисто-функциональном языке мутация весьма редка. Точнее в самом языке ее нет, но есть в реализации. Ну и некоторые другие языки также поддерживают shmem GC. Особая печалька состоит в том, что такие коллекторы не поддерживает LLVM, иначе все было бы просто. На самом деле, "неидеальный" GC подходящий для многопоточного shmem рантайма сделать не так уж и сложно - просто он будет консервативным, ну или mostly-copying. Такие языки даже есть, ибо libgc это поддерживает. Собственно проблема-то нифига не в алгоритме GC, а в кодогенераторе, который должен выдавать расположение ссылок на объекты кучи в стэке и в регистрах, а также делать спецуевую инструментацию. Для функциональных языков типа Хаскелла, это кстати не такая уж и проблема. Ибо спецуевая инструментация для парковки потоков в safe-point'ах им обычно не нужна, поскольку они перманентно выделяют память. Собственно, процедура выделения памяти и есть удобное место для парковки потоков. Хотя тут могут быть казусы, если компилятор Хаскелла окажется слишком умным и вычистит нахрен выделение памяти в какой-то долгоживущей функции :). Вот в этом месте возникла какая-то историческая хуйня которая застопорила прогресс. Уточним в чем собственно проблема. "Хороший" GC должен уметь отличать ссылки на объекты от других данных, т.е. быть точным. Иначе, ему приходится трактовать непонятные биты как возможные сцылки на жывые объекты, при этом он не может эти объекты перемещать. А это некузяво ибо перемещение объектов имеет преимущества: во-первых, локальность данных в памяти, во-вторых дефрагментацию, а в третьих - очень быстрое выделение памяти для generational GC, фактически такое же быстрое как и размещение на стэке. Однако, если в nursery - т.е. там где происходит выделение новых объектов, остались старые объекты, на которые ссылаются бит-паттерны, то выделение памяти затрудняется - нужно обходить эти устаревшие объекты. В принципе в случае CLR такие объекты могут быть по другим причинам, если их сделали pinned. Фактически, GC для CLR являются mostly copying а то и вообще консервативными. Но все равно желательно уменьшать кол-во возможных pinned объектов. А для этого кодогенератор должен выдать точное расположение ссылок на стэке и в регистрах для каждой инструкции. Понятно, что хранить такие мапы для каждой инструкции неразумно, посему возникло понятие safe-point'а и safe-region'а, для которых кодогенератор такие мапы выдает. Обычно это точки перед вызовом метода, возврат из метода и обратные дуги циклов. Однако safe-point'ы породили другую проблему - нужно теперь как-то вынудить треды остановится именно в safe-point'ах, а не абы где. В принципе эта задача относительно просто решаема, просто надо погреморроится. Либо тупо эммитировать проверки в safe-point'ах, что немного снижает производительность, либо модифицировать код trap'ами на ходу, что чуть геморройнее, но пошустрее. В функ языках, как я уже писал выше поступают проще - там safe-point на очередном выделении памяти, что правда не совсем надежно в случае продвинутой оптимизации. Вот сцука LLVM и не умеет эммитировать инструкции в safe-point'ах а также считать их для циклов. Также он не умеет делать liveness анализ и похоже не умеет делать map'ы для регистров. Вообще мне проблема кажется несколько надуманной. Хранить мапы для каждой инструкции действительно накладно и избыточно. На самом деле, хранить нужно для ключевых точек, а для остальных не сложно вычислять. Дело в том, что кодогенератор по любому нужную информацию имеет - ибо вся нужная информация генерится при назначении регистров и оптимизации. Соответственно, есть некоторые ключевые точки - переходы между базовыми блоками (линейный кусок инструкций без бранчей и входов), для которых мапы нужно считать по любому, а мапу для любой инструкции внутри блока несложно посчитать на основании мапы вначале/вкнце блока. Грубо говоря, инструкция может либо "рождать" ссылку на объект (например скопировать), либо может "убивать" ссылку, т.е. затирать ее нулем или другой ссылкой, ну или и то и другое. Причем последнее (livness) считать не обязательно, но желательно. Соответсвенно, алгоритм для реконструкции мапы для любой инструкции элементарный - определить базовый блок, содержащий инструкции, взять мапу для начала блока, для каждой инструкции от начала блока до текущей, добавить в мапу информацию о создаваемых инструкцией копиях. Ну и пройтись с конца блока, добавить еще жывые на данный момент сцылки (которые убъются последующими инструкциями). Вот и все (только еще учесть что инструкция может и генерить и убивать ссылки, так что тут есть легкий трик). Собственно, реализовать такой алгоритм для оптмизаторщегов и кодогенераторщегов вообще не проблема, ибо они так и делают, только для других видов анализа - часто анализ считают для базовых блоков, а потом пересчитывают для инструкций внутри блока - так быстрее, ибо внутри блока не нужны итерации. Для систем типа LLVM это неплохо бы сделать, ибо можно останавливать потоки в любом месте. Хотя для JIT'а, все равно может оставаться необходимость в инжекции/патчении кода на ходу. Продолжение следует (2 Comments |Comment on this)
Monday, May 14th, 2012
11:33 pm	Сборка мусора в случае когда много потоков одновременно лазиют в общую кучу (с мутацией) - весьма нетривиальная задача. По сути, таких систем не так много. Мне известны лишь JVM, CLR, Poly/ML, возможно Хаскелл. Хаскел поддерживает SMP но неизвестно мутируют ли его потоки общую кучу, т.к. язык вообще говоря чистый, так что может и не мутируют. Все остальные мне известные, либо тупо не поддерживают SMP, исключая параллельность общим локом (OCaml, SML кроме Poly/MLб Питон, Руби и т.д. и т.п.). Либо поддерживают SMP, но без общей кучи, к примеру, Erlang и Go. В принципе для большинства случаев это самый лучший вариант - лазить одновременно в кучу занятие не для слабонервных. Есть конечно наверняка еще какие-то язычки, где совместный доступ в кучу поддерживается одновременно с GC. Например какие-то Лиспы должны уметь, но я не в курсе. LLVM хотя и поддерживает GC но на данные момент фактически не поддерживает многопоточного мутатора. И непонятно когда будет. Вобщем создаие такое системы есть существенная проблема, на данный момент. Но хочется. И вот почему. Возьмем к примеру веб-сервера ну или системы обработки запросов. Часто их пишут в стейтлесс стиле, типа стейт хранится в БД/кэше/сессии. Удобно и масштабируемо, в том, смысле что проблемы масштабирования перекладываются на БД/кэш. На самом деле, понятно, что это тормозной способ, ну и стейтфул сервак вполне может быть быстрее десятка стейтлесс. В принципе, для крупных веб-систем все равно нужно много серваков (например чтобы IO масштабировать), но гонять стопиццот тормозных стейтлесс PHP серваков по любому будет накладно. Т.е. если шарить общие данные, как read-only так и mutable, в рамках одного процесса, для кучи параллельных обработчиков - это очень и очень существенный выигрыш, как по скорости, так и по экономии памяти. А ПХП стайл подразумевает шаренье через кэш и БД, что требует затрат на серилизацию данных, пересечение границы процесса, часто передачу через сеть, ну и наконец декодирование. В принципе, шаренье данных можно неплохо организовать и в акторской парадигме, т.е. когда мутаторы умеют изменять исключительно свои данные, а для прочих целей обмениваются сообщениями. С другой стороны, кэш либо БД будут работать шустее в случае если мутаторы умеют параллельно лазить в общую кучу. Ну т.е. большинство активных объектов должно общаться в стиле (однопоточных) акторов, но отдельные компоненты неплохо бы сделать многопоточными. При этом все в рамках одного процесса. Тут похоже единственные варианты пока - JVM и CLR. Возможно с какими-то оговорками Poly/ML и Haskell. Однако, в связи с моим предыдущеим постом, появляется еще одна возможность. Допустим большинство активных объектов системы есть куча однопоточных сущностей, которые вообще не имеют состояния. Т.е. в процессе обработки они что-то выделяют, меняют, но потом это все грохается. А выживают лишь сообщения, отданные наружу. При этом есть специальные stateful объекты, которые одновременно и многопоточно мутируются по просьбам других объектов. Причем не обязатльно через передачу сообщений. Причем в рамках одного процесса. Понятно, что для стейтлесс активных объектов управление памятью несложное, либо вообще не нужно. В любом случае genGC в однопоточном случае не есть проблема. Но для многопоточных stateful объектов нужна полноценный GC способный работать в в случае многопоточного мутатора. Однако, если ослабить требования к его производительности, то такой GC сделать сильно проще. Иными словами сложно сделать быстрый GC в случае многопоточного мутатора. Поскольку GC общий на всю систему, то он должен быть быстрым, иначе будет тормозить все. Однако, если для разных изолированных компонентов можно назначить свой GC то проблема упрощается. Т.е. в идеале бОльшая часть компонентов однопоточны и обмениваются сообщениями - иначе их просто сложно программировать. Для них достаточно простых (и быстрых) схем управления памятью, а иногда даже и примитивных. А несколько более медленный сборщик мусора для многопоточных компонентов не будет проблемой, ибо затронет лишь часть системы, подразумевается что небольшую. Вернее это будет меньшей проблемой, нежели пересечение границы процесса, с сериализацией/десериализацией и проч. И также возможно будет компесировано более быстрыми локальными схемами управления памяти у других активных объектов, где не требуется поддержка многопоточности. (1 Comment |Comment on this)
6:28 pm	Веб-сервера в некотором роде являются soft real-time системой. Просто у них время ответа можно сделать подольше чем в традиционных риал-тайм системах, но все равно есть ограничения, которые превышать не желательно, чтобы не напрягать йузера. Вобщем типичная обработка запроса должна быть достаточно быстрой, но не требуется из-зо всех сил снижать время обработки запроса (все равно куча времени уйдет на перекачивание данных по сети) - типично для риал-тайм систем, предсказуемость важнее производительности. В этом плане, для веб-систем, ну и обобщенно, для некоторых типов систем обработки запросов, можно сделать особые виды Garbage Collector'ов, заточенные под специфичные особенности веб-серверов. Очень часто веб-сервера делаются stateless, т.е. данные храняться где-то еще, а не в рамках серверного процесса: БД, кэш, куки, урл. Какой отсюда вывод? Гарбидж коллекция для стейтлесс сервера вообще нахуй не нужна - то что он на генерил, можно снести одним махом после обработки запроса. Так как он принципиально стейтлесс - то ничего и спасать не надо, следовательно все есть мусор. Разумеется, могут быть случаи когда сборка мусора все-таки нужна, но это скорее относится к разряду патологии - черезвычайно много хлама генерится в программе. Хотя конечно могут быть варианты, когда память достаточно сильно ограниченна (в пересчете на процесс), а он может генерить прилично хлама, который в ресурс памяти не влезает. Но в целом мне это представляется скорее патологичным случаем, откровенно хуевым дизайном кода, библиотек, языка, рантайм системы. Второй момент - в принципе можно все данные размещать на стэке :). Т.е. когда будем выходить из функции обрабатывающей запрос, то все это дело и свернется нахуй. В принципе, можно даже tail call'ы не оптимизить. Разумеется, тут понадобится приличный размер стэка, что не очень удобно, особенно если много потоков (а в дубовых языках это так). Однако, есть новомодное веяние - в Go к примеру, стэк выделяется фрагментами. Т.е. как только стэк готов переполнится - добавляем новый фрагмент. Фактически, стэк содержится в куче, только не фреймами по отдельности (как в некоторых stackless системах), а блоками. Итого, можно все данные выделять на стэке, а стэк выделять из кучи. Возможно за исключением больших массивов. Вобщем и целом, при таком подхоже сборка мусора либо вообще не нужна, либо сильно упрощается. Ибо сборка мусора для больших данных не так уж и сложна, ибо происходит редко. При этом подход годится и для стэйтфул процессов - нужно просто собирать мусор при сворачивании стэка, как это к примеру делается в некоторых реализациях Схемы. Т.е. стейт храним в куче, локальные данные - на стэке. Для того чтобы отличить стэйет, его как правило нужно явно или неявно пометить (записать в БД/кэш) и т.д. Т.е. опять-таки упрощается дизайн GC - то что нужно спасать явно или неявно помеченно программером, либо системой вывода типов. Ну так же в куче (возможно специального вида) нужно хранить большие куски данных и куски стэка. Этот подход также можно описать иерархическими регионами + сборка мусора, как это к примеру сделано в MLkit. Т.е. тут явно есть по крайней мере два типа региона: один для обработки запросов, и второй для состояния процесса, если оно есть. В прицнипе, гарбиджколлектить можно оба региона. Но как я писал выше, обычно для запросного региона можно выкинуть весь хлам в конце. Ну а стейт надо гарбидж коллектить понятное дело. Также под сию систему пытается заточится generational GC. Но у него нет знаний о том, какие данные являются локльными для процесса, а какие - состоянием. Поэтому у него это получатеся делать не так идеально как могло бы (но в целом очень даже хорошо). Интересным в данной схеме является также возможность реализации конкурентных GC с малыми паузами. Поскольку доступ в главный регион с состоянием явно или неявно помечен, а также достаточно редок, то можно использовать read-barrier'ы на чтение состояния. Для веба это вполне естественно запросы в БД/кэш отличаются от локального доступа. А на рид-барьерах конкурентный коллектор сделать проще. Обычно их избегают в силу тормознутости рид-барьеров и того что операции чтения самые частые. Однако если это делать только для стейта, запросы к которому достаточно редки, то это не будет проблемой. И последнее что хотелось бы отметить: коли у нас фактически стэклесс, то легко сделать континюации, а значит и всякую асихнхонную хрень (что для веб очень в плюс) и акторов, а также можно применить континуации для реализации долгоживуших веб-"транзакции", когда одна форма обрабатывается в течении кучи запросов, для чего континюации подходят весьма естественно. Разумеется, тут будут сложности с тем, что подвешенная континюация уже относится к стейту и будет хранится в главном регионе, что повлияет на сложность системы обработки памяти. Но это уже не принципальные вопросы. (3 Comments |Comment on this)
Tuesday, May 1st, 2012
11:35 pm	Суперкомпиляция, верификация, тестирование, трансформация моделей Я раньше считал суперкомпиляцию замыканием множество обычных оптимизаций, типа частичной эвалюации. Хотя обычно их различают, хотя я все же склоняюсь к мнению что сие есть следствие конкретных структур данных, используемых в процессе оптимизации, а также алгоритмов. Грубо говоря, очень сложно реализовывать многопроходные перемежевывающияся анализ и трансформации, которые сами по себе очень сложны. Вобще на данный момент я тоже склонен рассматривать супероптимизацию отдельно. А это я все к тому, что я обнаружил, что одна из интересных мне проблем как раз решается методиками типа суперкомпиляции. В то же время такие преобразования весьма похожи на те, что делаются при доказательстве функ программ в Coq. Что не удивительно. Ведь оптимизация - это трансформация, сохраняющая семантику программы. А верификация часто состоит в том, чтобы доказать что одна функция эквивалентна другой, что можно делать трансформацией (сохраняющей семантику). В то же время еще Турчин указывал, что суперкомпилятор вполне может использоваться как автоматический доказатель теорем. Вобщем, на данный момент, глобальная коммунистическая цель (которая на горизонте, и в процессе достижения которой кормить не обещали), состоит в соединении функционалки, императивки, верификации, суперкомпиляции, тестирования, трансформации моделей, ну и проч хуйни в единое целое. Общее описание коммунизма примерно такое: 1 модели в том числе можно задавать функ языками 2 модели в частности могут выступать в роли спецификаций 3 модели могут транслироваться в исполнимый код - предпочтительно, но не обязательно 4 желательно совмещение функционалки с императивкой - тут нужен отдельный пост Цель сего блока - уменьшить затраты на формальную спецификацию, верифкацию а также тестирование. Фактически, сие можно рассматривать как прототипирование, в случае исполнимых спек. Далее идет итеративное развитие прототипа в более крутую реализацию. Тут применяются: 5 трансформации моделей 6 верификация эквивалетности моделей, иногда полуавтоматическая 7 тестирование эквивалетнотсти моделей, полуавтоматическое (генерация тестов автоматическая) 8 всяческие оптимизирующие преобразования, включая суперкомпиляюцию, например, для получения императивного кода 9 но также и для верификации/тестирования соответствия функциональных и императивных моделей В краткосрочном плане, интересна подзадача трансляции функциональных программ в читабельные императивные, желательно с деструтивными апдейтами. Сие позволит упростить задачи верификации, тестирования и спецификации иперативного кода. Да и написания вобщем-то тоже - на функ языках писать удобнее. Путь примерно такой: 1 func -> CPS 2 CPS -> CPS' суперкомпиляция, оптимизация, инлайнинг 3 CPS' -> CFG 4 CFG -> CFG' - оптимизация инлайнинг 5 CFG' -> imperative code более-менее читабельный 2,3,4 возможно надо будет проделывать итеративно несколько раз (Comment on this)
5:21 am	Доделал программу для восстановления структуры циклов из CFG. Типа чтобы было while/if/do-while/break/continue, без goto вобщем. Правда кое-какие фичи не охваечены, типа брейки из нециклов. Циклы вроде как правильно обрабатывает на удвиление, по крайней мере, те двухцикловые, включая хитрожопые конструкции которые я протестил. Пока не хватает реконструкции сложных условий а ля (a && b) ну и приведения хитрожопых break|continue в более читабельный вид. Но это уже чисто читабельность, на компилябельность (джавы) не влияет. Изначально мне надо было для компилятора ПХП в Жабу - не хотелось с байткодом возится. Однако, спектр применений гораздо шире. Например, для приведения тяжело за-инланеного CFG и CPS в читабельный императивный вид (без goto). Например после устранения тэйл-рекурсии. В случае сложных CPS и неприведенных CFG конечно этой тулзы не хватит и надо будет как-то дорабатывать отсутствие goto. Ну это не так и сложно доработать будет при нужде. А при трансляции в байт-код и нужды в этом нет. (Comment on this)
Sunday, April 29th, 2012
9:17 pm	Сдается мне что трансляция в CPS убъет сразу много интересных мне зайцев. Во-первых, это метод трансляции близок к функ языкам. Во-вторых, он примерно эквивалентен SSA В-третьих, континьюации ползволяют описывать легковесные треды, ну т.е. абстрагироваться от них. В-четвертых, там удобно делать инлайны. В-пятых, можно и тайл-коллы устранить, заделать в циклы. В-шестых, эксепции там тоже описываются, и другие эффекты. В-седьмых, судя по всему из CPS удобнее генерить высокоуровневый код: if/while без джампов :) В-восьмых, для целей автомтизированного тестирования, это похоже тоже весьма удобно. Ибо можно анализировать структуру бранчей, а остальное представить континьюациями. (Comment on this)
9:10 pm	Ассерты и пре/пост-кондишены, которые встраиваются в исполняемый для тестирования и удаляются для продакшена, можно рассматривать как разновидность оптимизации. Т.е. код "собирается" вместе с проверками, но в случае оптимизации этот код удаляется. как ненужный. Примерно так же делается в Coq при экстракции программ. Одно из весьма желательных требований - чтобы программа с проверками и без оных работала точно так же, хотя бы без учета скорости и потребляемой памяти. Это можно достичь если проверки "чистые" - не меняют состояния программы, а только инспектируют. В случае многопоточности все конечно сложнее, но там проверки не спасут, по большому счету. Итого хорошо бы иметь чистый функ язык гармонично скомбинированный с императивкой, типа DDC (Disciplined Disciple Compiler). Ибо модели софта для проверок обычно удобнее писать функционально. Ну и существенную часть кода можно писать функционально. Ну и лишь некоторую часть - императивно, так ведь тоже хочется :). (Comment on this)
4:25 pm	Меня посетила очередная идея - затранслировать Жабу в Хаскель А точнее жабий байткод в ленивый код. К примеру, у нас есть код типа a = ..... b = .... if (c > 0) .... До того как мы бранчнемся в if(c>0) вычислять а и б нет нужды, да и потом тоже нет. Следовательно сей код можно передать дальше в виде функции, ну и когда надо вычислить. То бишь ленивость. Точнее это конечно же просто трансляция в CPS с некоторыми последующими трансформациями/оптимизациями. Однако оное весьма полезно для символического исполнения программы : ибо к примеру если мы хотим побегать по бранчам, то часть вычислений (вполне возможно непустую) можно и отложить. (Comment on this)
Saturday, April 28th, 2012
5:55 pm	AFCTest Добавил интерпретацию байт-кода, теперь тестовый метод исполняется в ЖВМ интерпретаторе. Конечно с кучей ограничений, зато удобнее хакать. (Comment on this)
6:56 am	Ну вот реализовал прототипчег могучего тестирования на основе CLP библиотеки для Жабы. Немножко конечно пришлось с мудреностью библиотечки поебаться, но это обычное дело для таких библиотек. Правда, почему-то у библиотечки домены не могут быть (MinInt..MaxInt), а слегонца поменьше, типа пару миллиардов в обе стороны. Суть ограничения мне пока не ясна, но думаю найдется библа у которой такого ограничения нет, по крайней мере на интервальных задачах. В принципе не так уж и страшно. Теперь надо бы сделать построение модели по коду, хотя бы примитивное. В принципе, можно обойтись инструментацией на первых порах. (Comment on this)
12:51 am	Набросал простенький и тупой прототип стохастического тестирования. Он генерит случайные число, тупо билдит по нему тест-кейс, генерализует его по модели (тоже тупой), ну и запоминает. Тупизна, зато быстро и просто. И сразу понятно куда двигать дальше. Тупая генерация конечно не катит. Так что надо добавлять констрейнт-солвер. Али еще какую заумность. Плюс анализ кода. (1 Comment |Comment on this)
Friday, April 27th, 2012
9:04 pm	Одним из достоинств моего "стохастического" "верификационного" тестирования является то, что обобщения не обязательно должны быть точными. Фактически при неточных обобщниях сей метод объединяет множество разных подходов к тестированию, включая эксплорационное и верификацию. Действительно, при верификации нам требуется точное обобщение и полное покрытие. Из этого мы получаем доказательство корректности. И наоборот из доказательства корректности можно получить "полное" покрытие. Экслорационное тестирование делает какой-нить ход, ну и выбирает по результатам куда тестить дальше. Собсно, "случайная" генерация тест-кейсов это и моделирует. Выбираем куда двигаться дальше ведь исходя из предположений о непокрытости. Генерация тестовых случаев на основе equivalence class partitioning, assertion testing boundary value analysis - то же самое. "Случайно" выбираем одно значение из требуемых классов, ну а дальше выбираем следующее из "непокрытых" классов. Тестирование с учетом метрик покрытия - генерим новые тест-кейсы так, чтобы они улучшили метрику покрытия - дошли до новых строчек или покрыли новые бранчи и условия. Генерация всеразличных попарных комбинаций - то же самое. Для каждого пары (троек и т.дю) значений делаем обобщение, что мы протестировали все случаи в которых присутствует сия пара (тройка и т.д.) Случайная генерация тесткейсов аля QuickCheck вообще очевидно. Прочие автоматные и модельные методы тоже сюда попадают. Просто нужно подобрать "случайность" и метод "обобщения". Кавычки ибо случайность не обязательно случайная, а обобщение не обязательно точное. Таким образом "стохастическое" "верификационное" тестирование является обобщенным подходом на все случаи жизни :). На самом деле, тут есть важный класс методов тестирования, который я не встречал в реальности. По крайней мере, так на вскидку не помню. Например, можно делать неточную, но консервативную оценку обобщения тест-кейса. Обычно при тестировании делают оптимистическую оценку, т.е. ну непротестировали что-то ну да и хрен с ним. Хотя верификация все-таки построена на консервативном обобщении, но оно обычно к разряду тестирования не относится :). А консервативные оценки в случае некоторых моделей разбиения выглядят очень даже интересно. Фактически можно делать одновременно и консервативную и оптимистическую оценку обобщения. В целом мне думается что этот метод очень хорошо подойдет как развитие идей QuickCheck'аю Оный очевидно делает много лишней работы и удобен для чистого декларативного кода. А фильтрация классов эквивалентности поможет применить его и для императивного случая. По крайней мере, широкий набор кусков кода, актуальных в реальности можно будет тестировать с большой уверенностью и даже полностью. (3 Comments |Comment on this)
8:22 pm	Об имплементационных апектах "верификационного" покрытия Допустим у нас есть "случайная" процедура генерации тестовых случаев. Она может быть не обязательно случайной, но мы ее в данном случае трактуем таковой. Далее, пусть у нас есть логический движок который умеет обобщать информацию, полученную из трейса исполнения, возможно с помошью хинтов (лемм) от пользователя, т.е. полуавтоматически. Часто это можно сделать, например если какие-то параметры не использовались в трейсе, то можно взять любые. Ну или если копировалось значение, то опять же можно взять любое. Допустим мы сгенерили "случайно" один тест-кейс. Теперь, если мы прогоним сей тест, то с помощью движка получим целый класс эквивалентности, который мы протестировали. Замечу, что следующий тест-кейс лучше сгенерить так чтобы он не попал в сей класс эквивалентности, ибо мы его уже протестировали. Поэтому и важна "случайность" - т.е. мы генерим "случайные" тест-кейсы пока не получим "новый", в том смысле что он не попадает в уже протестированный(ые) класс(ы). Случайный будет работать в общем случае, по крайней мере при невысоком покрытии. Разумеется можно применить и специализированные методы генерации тесткейсов за пределами класса эквивалентнсоти. Разумеется можно применять любой способ генерации тестов, ну и объединять обобщенную информацию о протестированном пространстве. Просто при таком подходе будет неплохо работать и случайная генерация. Дык вот. Допустим у нас теперь есть "стандартный" алгоритм разбиения тестового пространства на классы эквивалентности. Возможно параметрический. Понятно, что мы можем (в теории, при достаточно удобной форме разиения) выяснить какое кол-во стандартных классов покрыто, а какое нет. По крайней мере, такие разбиения придумать можно. Например можно применить метод Монте-Карло. Генерим уже по настоящему (псевдо)случайные тесты и смотрим какой процент из них попал в протестированное обобщенное множество. Можно также сравнивать с учетом дополнительного разбиения на "стандартное" покрытие. Т.е.если тест-кейс попал в стандартный класс эквивалетности и одновременно был (обобщенно) протестирован, то он считается покпытым. Если не попал - то непокрытым, но учтенным. Метрику можно считать как относительно полного кол-ва классов, та и только относительно учтенных. (Comment on this)
7:46 pm	"Verificational" Test Coverage wrt Specification Возникал идея метрики тестового покрытия. Допустим у нас есть спека. В некотором смысле, она всегда есть, ибо если нет - то любой код годиццо. Точнее нам нужна формальная спека, которая в случае тестов тоже всегда есть. Формальная спека может быть разных видов: 1 сигнатура метода - тоже между прочим спека, впрочем ее часто компилер проверяет 2 фиксированный набор значений параметров для которых точно известен правильный результат 3 обычно есть неявное требование отсутствия рантайм эксепций, крэшей и прочих кривых сайд-эффектов, т.е. появление оных по умолчанию есть нарушение неявной спеки, хотя иногда это правильное поведение 4 набор свойств, которым должен удовлетворять результат работы программы 5 набор свойств записанных декларативно, в виде предикатов к примеру 6 альтернативная реализация, которой должна удовлетворять прога, возможно по каким-то проекциям, а не 100% Вобщем не суть важно, главное что есть формальная исполнимая процедура, которая будучи применена к набору параметров результатам (включая возможно сайд-эффекты), говорит соответствует ли оно спецификации или нет. Хотя возможен и результат типа "неприменимо", типа спека этого формально не требует. К примеру есть фиксированный набор параметров и ожидаемых результатов (заданных константами, а не процедурно). Если мы исполняем код с каким-то другим набором параметров, то формальная спека нам ничего точно сказать по этому поводу не может, ибо она на неопределена. Ну дык вот, это было лирическое отступление, а теперь ближе к суть. Есть стандартная метрика покрытия, которая говорит, какая часть кода была задействована в тесте. А где спрашивается метрика, которая бы говорила насколько покрыта спека? Это еще не совсем "верификационное" покрытие, но уже ближе к нему. В принципе, если формальная процедура проверки резльтатов на том же языке, то и тестовое покрытие точно так же можно померить. Т.е. нужно применить процедуру проверки к тестируемой функции и потребовать, ну и померить покрытие комбинированного кода (за исключением всяких вспомогательных функций). Для формальных проверялок на других языках тоже вобщем-то можно померить покрытие основываясь на коде. Конечно это далеко не идеальная метрика, но не так уж и плохо. Однако, допустим спека задана с помощью логики предикатов. Если взять модель кода выраженную также в логике предикатов (оставим пока вопросы реализуемости такого подхожа), то можно опять-таки скомбинировать их в единую модель, разбить эту логическую модель на классы эквивалентности (опять-таки проигнорируем пока вопросы реализуемости). Ну и замерить кол-во классов, для которых имеется хотя бы один тест. Вот если это число поделить на общее кол-во (желательно конечно непустых) классов и будет то что я бы назвал "верификационной" метрикой тестового покрытия. "Верификационной" метрикой я называю из следующих соображений. Допустим есть доказательство корректности программы. Если целевую теоррему представить в виде A&B&...&C -> D|E|...|F, то его можно преобразовать к виду ~A|~B|...|~C|D|E|...|F. Фактически доказательство состоит в разбиении пространства интерпертаций на классы эквивалентности, ну и предоставлении свидетельства, что для каждого класса эквивалентности верна хотя бы одна формула из списка. Фактически, набор классов можно еще раз разбить на подклассы, так чтобы каждый делал верным определенную формулу из списка. Итого получается что для любого возможного значения есть такой подкласс, который делает верным либо CD...F либо неверным AB...C. Ну и соответственно для каждого из этих подклассов есть тест-кейс. Это быдет в некотором смысле идеальное тестовое покрытие, ибо любой другой тест-кейс попадет в уже покрытый (под)класс эквивалентности. Соответственно, "верификационная" метрика будет грубо оценивать степень приближения к такому идеалу. Ну и разумеется говорить, где надо искать непокрытые случаи, ибо тестировать покрытые (под)классы уже не так интересно. Еще одним интересным моментом является о, что доказательство того что какая-то целевая формула верна на каком-то конкретном (полд)классе эквивалентности является символическим исполнением программы для всех значений из данного (под)класса. Т.е. такое тестовое покрытие будет полным в том смысле, что мы реально исполняем по одному тест кейсу из каждого (под)класса, ибо реальное исполнение для всех членов (под)класса невозможно либо слишком затратно в общем случае. Еще один интересный момент, заключается в том, что конкретное исполнение на конкретном тест-кейсе можно обобщить до целого класса эквивалентности. Если это можно сделать для полного покрытия (т.е. объединение выведенных классов эквивалентности равно множеству интерпретаций), то мы получаем доказательство корректности реализации по отношению спецификации. (Comment on this)
6:02 pm	Хаскел видимо самый крутой язык, по крайней мере, результаты программирования на нем мне нравятся больше всего. Код могуч и продуман, как правило. В частности, это вызвано тем что на Хаскелле абы кто не пишет, но на самом деле, Хаскелл диктует такой стиль программирования. Еще более круты конечно языки типа  Coq/Agda и проч. Они даже компиляются во что-то практичное. Но все-таки они пока слишком академичные, в том плане что ваять код на них сложно. Но результаты и экспириенс еще круче, по крайней мере, в каких-то аспектах. Все-таки мне думается интенсиональная теория типов, несмотря на свои полезные свойства к обычному программированию не очень хорошо привязывается. А у экстенсиональной свои проблемы. Свежие решения есть, но они пока не зрелы. Тем не менее уже сейчас понятно, что верифицированное программирование вполне реально и применимо. (Comment on this)
5:28 am	Переделал мою любимую ПХПшную прогу прогу на DDC который диалект Хаскелла с деструктивными апдейтами. Результат впечатлил. Во первых код практически очень близок к исходному. Во-вторых работает ровно с такой же скоростью :). Т.е. вообще один в один практически. Оно и понятно, в DDC используется boxed представление, примерно такое же как и в ПХП. Но есть возможность писать и unboxed. Переписал. Однако, это уже не императивное программирование получается, ибо анбоксед DDC не дают апдейтить, так что пришлось переписать в функ стиле, рекурсивные функции и все-такое. Вернее частично функционально. Стало работать в 7-8 раз быстрее. Правда, из-за баги в компиляторе целиком исправить не удалось. На самом деле, такой код от обычного Хаскелла не отличается - там тоже есть анбокседы, так что смысла особо городить огород нет. Точнее конечно все же есть :) При более внимательном рассмотрении выяснилось, что DDC делали попроще, так что его нонешний код эффективной компиляции не предусматривает похоже, ибо транслируется в подмножество Си ну и не самым эффективным способом. Хотя возможность такая судя по всему есть. А жаль. Но идея все равно хорошая. Нужно только кодогенератор переписать. Вобщем по идее надо переписать бэкенд из DDC Core в CMM или LLVM. Тогда по идее должно быть пучком. Кстати CMM создавался с ровно теми же целями, что нужны мне, но статус его не определен. В GHC похоже используется свой собственный транслятор CMM в ажно три разных дальнейших вида (ASM/LLVM/C). Кроме того они там чего-то мутят насчет нового бэкенда. Хотя задействовать конечно можно и Хаскеловский CMM - штука очень хорошая, ну и перспективная (новый крутой Хаскеловский бэкенд). Впрочем есть подозрение что LLVM будет не сильно хуже. (Comment on this)
Thursday, April 26th, 2012
2:19 pm	Самым интересным из реалистичных, срецтв для записи алгоритмов выглядит DDC в силу того что совмещает императивность и функциональность. Ну и DDC Core вполне тянет на роль промежуточного языка. На первый и второй взгляд, он удовлетворяет (может удовлетворить после доработки напильником) всем моим целям. (5 Comments |Comment on this)