Russian researcher blog

Programs That Test Themselves (2009)

2010-12-25T23:50:00.000+03:00

http://se.ethz.ch/~meyer/publications/computer/test_themselves.pdf

В статье описывается система AutoTest, позволяющая повысить эффективность использования программных контрактов. Система позволяет:
1) автоматически генерировать test case'ы (в основном, случайным образом выбирая аргументы вызываемых методов)
2) следить за работой программы и генерировать test case'ы, на которых произошли precondition failure или postcondition failure
3) вручную задавать test case'ы.

Задача построения идеального транслятора для VLIW-архитектуры

2010-12-12T13:08:00.000+03:00

Для ускорения выполнения последовательная программа исполняется современными микропроцессорами почти всегда с использованием различных методов явного или неявного распараллеливания. Задача состоит в том, чтобы в явном виде подготовить исходную последовательную программу в таком виде, чтобы максимизировать ее распараллеливание на микропроцессоре. Естественно, задача имеет смысл только при задании класса архитектур и класса программ.

Задача верификации спецификаций

2010-12-02T23:27:00.000+03:00

Для верификации программ придумано множество различных методик. В том числе, например, "верификация на модели" (model checking), когда верифицируется не сам код программы, а его модель (обычно некая система переходов или автомат специального вида). На таких моделях успешно проверяется выполнение ряда свойств (например, отсутствие взаимоблокировок, дедлоков, в мультипроцессном коде).

Но почему бы не посмотреть на верификацию спецификаций? Ведь для спецификаций тоже можно формулировать свойства и проверять их! Задача состоит в определении таких свойств и предложению методов верификации спецификаций на выполнение этих свойств.

Сложность:
постановка задачи (непонятно, что это за свойства, о каких спецификациях идет речь)
вычислительная сложность (как и любая верификация)

Задача автоматического поиска обобщенного состояния

2010-12-02T23:23:00.000+03:00

Речь идет о тестировании программ. Программы запускаются различными способами и проверяется, что во всех этих запусках программы ведут себя так, как положено. Вопрос только в том, что это за способы и как реализовать эти способы (задача проверки работы программы решена куда лучше).

Рассмотрим программу (или компонент программы), поведение которой описывается конечным автоматом. Тогда под "способами" можно понимать запуски, в которых достигаются заданные состояния автомата, переходы в автомате или даже целые пути. Но проблема в том, что размеры автомата огромные. Поэтому состояния автомата группируют согласно некому отношению эквивалентности и полученный автомат называют "обобщенным автоматом". Задача состоит в автоматическом построении таких обобщенных автоматов. Обобщенный автомат не должен стать недетерминированным, если исходный был детерминированным, ну и количество состояний в обобщенном автомате должно-таки позволять проводить тестирование в приемлемые человеческие сроки.

Сложность:
постановка задачи (четко надо понять, какие автоматы называются "обобщенными" и о каком отношении "обобщения" идет речь),
вычислительная сложность (перебор всех разбиений множества состояний автомата)

Задача автоматического поиска дефекта в программе

2010-12-02T23:14:00.000+03:00

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

Сложность:
вычислительная сложность (перебор всех входных данных)

Задача автоматического распараллеливания последовательных программ

2010-12-02T23:08:00.000+03:00

Есть такая светлая идея, что последовательный алгоритм может быть эффективно распараллелен. Конечно, речь идет о специальных параллельных архитектурах и о специальном классе последовательных алгоритмов. Задача состоит в том, чтобы выделить такие классы программ и архитектур и предложить методы автоматического распараллеливания.

Сложность:
сложность постановки задачи,
вычислительная сложность

Проверка корректности самоизменяющихся программ

2010-12-02T22:29:00.001+03:00

Задача состоит в том, чтобы по данной программе (возможно, лишь в бинарном виде) определить:
1) портит ли она "полезные" данные (т.е. есть данные, которые она портить не должна)
2) передает ли она несанкционированным образом третьей стороне какие-либо данные

Примеры самоизменяющихся программ: вирусы

Синонимы: "полиморфный" код (то же, что и самоизменяющийся)

Сложность:
сложность постановки задачи (неточно сформулировано то, что надо проверять),
вычислительная сложность (проанализировать все пути выполнения)

Howto integrate Google Code's bug tracker and Eclipse

2010-06-27T13:32:00.005+04:00

http://blog.vortex64.ru/?p=41 (in Russian)

Eclipse 3.6

2010-06-23T21:26:00.007+04:00

is released !

and crash is occured in my Ubuntu Lucid !
#
# A fatal error has been detected by the Java Runtime Environment:
#
# SIGSEGV (0xb) at pc=0xb7807f2d, pid=27481, tid=3077183168
#
# JRE version: 6.0_18-b18
# Java VM: OpenJDK Client VM (14.0-b16 mixed mode, sharing linux-x86 )
# Derivative: IcedTea6 1.8
# Distribution: Ubuntu lucid (development branch), package 6b18-1.8-0ubuntu1
# Problematic frame:
# C [libpthread.so.0+0x7f2d] pthread_mutex_lock+0x1d
#
# An error report file with more information is saved as:
# /tmp/hs_err_pid27481.log
#
# If you would like to submit a bug report, please include
# instructions how to reproduce the bug and visit:
# https://bugs.launchpad.net/ubuntu/+source/openjdk-6/
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#

another crash:
#
# A fatal error has been detected by the Java Runtime Environment:
#
# SIGSEGV (0xb) at pc=0xb76c3f2d, pid=28752, tid=3075856064
#
# JRE version: 6.0_20-b02
# Java VM: Java HotSpot(TM) Client VM (16.3-b01 mixed mode, sharing linux-x86 )
# Problematic frame:
# C [libpthread.so.0+0x7f2d] pthread_mutex_lock+0x1d
#
# An error report file with more information is saved as:
# /home/kornevgen/hs_err_pid28752.log
#
# If you would like to submit a bug report, please visit:
# http://java.sun.com/webapps/bugreport/crash.jsp
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#

Solution:
My Ubuntu had xulrunner-1.9.1 and xulrunner-1.9.2 simultaniously. Solution is removing xulrunner-1.9.1 :)

New York Times о тестировании микропроцессора Intel

2009-06-13T14:50:00.002+04:00

статья от 17 ноября 2008 года
http://www.nytimes.com/2008/11/17/technology/companies/17chip.html?_r=3&pagewanted=1&adxnnlx=1226923276-C0QeFwmZpPS2IDCHprvvYg
(via Zvonimir Rakamaric)

Философия прототипа

2009-06-11T09:59:00.002+04:00

Недавно для себя уяснил очень важную мысль (вообще-то, ее мне должны были привить еще во время обучения, ну ладно, сейчас не об этом) : на начальной стадии необязательно и не нужно реализовывать систему целиком! Достаточно написать прототип, который будет работать на некотором наборе тестовых (показательных) примеров.

А уже опосля, когда будет принято утвердительное решение о реализации, выделены ресурсы (время, деньги, люди) и уточнены требования, тогда уже можно браться за серьезное программирование.

Компиляция и сборка с MinGW

2009-05-30T13:22:00.003+04:00

по-моему, неплохая статья http://www.crossplatform.ru/node/58

И вновь про двойную диспетчеризацию на Java

2009-05-27T14:11:00.002+04:00

Пусть надо реализовать функцию от двух переменных f(X, Y), где типы X и Y - суть корни деревьев наследования, причем так, чтобы при появлении нового типа X или Y компилятор нам сам подсказывал, что надо дописать. Обычная стандартная задача двойной диспетчеризации :) Не претендуя на всеобщий ее охват, напишу примененный мною метод реализации такого механизма. Добавлю только, что типы X и Y абстрактные.

Итак, в типе

Определяю новый тип (interface) YVisitor:
public interface YVisitor
{
void visitY1( Y1 y );
void visitY2( Y1 y );
}
помещаю туда методы про те потомки типа Y, которые вспоминаются.

В тип Y помещаю абстрактный метод:
public abstract void visit( X x );

Тип X делаю implements YVisitor и добавляю метод

public void f( Y y )
{
y.visit( this );
}

В каждом потомке типа Y нужно теперь реализовать метод visit. Делаем это по такой схеме, для примера на классе Y1:
class Y1 extends Y
{
...
public void visit(X x)
{
x.visitY1(this);
}
}
Очень важный момент, что суффикс имени вызываемого метода должен содержать имя класса (потомка Y)! Если такого метода нет в классе X (а это означает, что еще нет соотв.visit-метода в интерфейсе), то идем в интерфейс YVisitor и добавляем метод void visitY1(Y1 y1); Таким образом, при добавлении нового потомка типа Y такая схема работы позволит отследить весь необходимый новый код.

Кроме того, компилятор будет требовать реализации методов visitYi в каждом потомке типа X. Если появится новый потомок типа X, компилятор сообщит, что в нем нужно реализовать все visitYi.

Вызвать это дело следует так: x.f(y), где x типа X, y типа Y.

Как использовать Yices из Java под Windows

2009-05-26T10:56:00.002+04:00

Yices - SMT-solver от Computer Science Laboratory SRI International ( http://yices.csl.sri.com/ ). Иными словами, этот инструмент предназначен для решения задачи SAT, но с оптимизациями в некоторых теориях (например, битовые вектора, целые числа). Инструмент не является (пока) open-source. К дистрибутиву поставляется библиотека (dll и so) для вызова Yices из программ на Си. Мне же нужно было вызвать ее из Java, для чего пришлось воспользоваться механизмом JNI. Но для этого нужен архив объектных модулей (".a"), который отсутствовал в дистрибутиве. Коллеги из PACE University сделали уже готовую JNI-оболочку для вызова Yices из Java ( http://atlantis.seidenberg.pace.edu/wiki/lep/Yices%20Java%20API%20Lite ), однако на их сайте были представлены только jar под Linux, а, поскольку, потенциальные пользователи моей программы работают под Windows, то надо было ее пересобрать для Windows. К счастью, PACE University предоставляет исходники JNI-оболочки бесплатно, чем я и воспользовался.

Итак, качаем http://atlantis.seidenberg.pace.edu/~lep/yices/codes/source.tar.gz , распаковываем.
я собирал под MinGW 5.1.4 (под cygwin не получилось).
Если у вас не установлен JDK, сделайте это - его header'ы потребуются при компиляции оболочки. я для простоты поместил в директорию include из sources.tar.gz содержимое директории include (c win32) из JDK (в моем случае 1.6.0_13).

подготавливаем libyices.a - коллеги его уже подготовили для нас и поместили в директорию lib архива sources.tar.gz. (иначе пришлось бы возиться с reimp и dlltool)

компилируем оболочку (прилагаемый Makefile, как выяснилось, не подходит для компиляции под Windows):

gcc -o libYicesLite.dll -shared YicesLite.c -Iinclude -Iinclude/win32 -Llib -lyices -Wl,--add-stdcall-alias

(последний параметр очень важен - без него не получится вызвать функции оболочки из Java!)
эта команда может выдать набор предупреждений, но никаких ошибок не должно быть (иначе не появится dll)

теперь компилируем java-исходники:

javac yices\YicesLite.java

обратите внимание, что YicesLite.java именован именно так и в этом пакете. Менять имя пакета и имя класса НЕЛЬЗЯ - под эти имена сгенерирована оболочка на Си, под эти имена мы только же компилировали dll.

Теперь можно написать тестовый пример и запустить его :) Только не забудьте сделать очень важную вещь: поместить скомпилированный libYicesLite.dll в директорию из переменной среды java.library.path и libyices.dll (ее можно скачать с сайта Yices) в директорию из переменной среды PATH (чтобы она могла подгрузиться, как зависимость). И еще проверьте, как вызывается метод System.loadLibrary! Для данных имен правильным будет вызов

System.loadLibrary("libYicesLite")
(с префиксом lib!!!)

Теперь, кажется, всё :)
скачать libYicesLite.dll и соответствующий jar под Windows можно тут: http://tesla-project.googlecode.com/files/libYicesLite.dll
http://tesla-project.googlecode.com/files/YicesLite.jar