2008-10-30 Michael Weber * Released version 1.2.9 2008-10-30 Michael Weber * tests/spin/benchmark.sh: new environment variable NIPS_VM_OPTIONS * Implement machinery not to store atomic steps. Not storing atomic steps can safe massive amounts of memory. Callbacks can force to VM to continue execution of any step by returning IC_CONTINUE_INVISIBLY. * search.c: note that the way these searches are implemented, this can potentially lead to non-termination in the presence of a non-terminating loop completely contained inside atomic sections. Changed output "states visited:" to "states stored:". Transitions continued with IC_CONTINUE_INVISIBLY are not counted as "transitions visited" in the final statistics. The sum of "transitions visited" and "atomic steps" is the number of visible transitions. * tests/spin/benchmark.sh: adjust for changed output. * main.c: new option -no-store-atomic-steps 2008-04-16 Michael Weber * Released version 1.2.8 2008-04-15 Michael Weber * Makefile: linker flags updated for darwin9 (MacOS X 10.5.2) 2007-06-07 Michael Weber * Support for SCC decomposition information of control-flow graphs of all processes, the monitor process probably being the most interesting one. The actual information is supplied by SARN. * state.c (nipsvm_state_monitor_scc_id): added * bytecode.c (bytecode_scc_map, bytecode_scc_type) (bytecode_scc_weak_graph): added * nips_asm.pl: if set, add NIPS_HOME to path 2007-03-27 Michael Weber * Released version 1.2.7 2007-03-26 Michael Weber * nipsvm.c (simple_error_cb): added, fixes segfault in error callback which received the wrong context; reported by 2007-03-10 Michael Weber * Released version 1.2.6 * search.c (search): silenced warning on MacOS X * instr_step.c (instr_succ): code cleanup: p_monitor * Makefile (LDFLAGS_LIB): MacOS X support 2006-07-06 Michael Weber * nips_disasm.pl: emit !modflags only if non-empty * nips_asm.pl: if set, use NIPS_HOME to locate *.pl files 2006-06-27 Michael Weber * main.c: adjusted version * search.c: initialize n_atomic_steps to zero (lost in last commit) 2006-06-06 Michael Weber * Released version 1.2.5 * search.c: count and print number of atomic steps. 2006-05-19 Michael Weber * nipsvm.c (nipsvm_default_error_cb): removed extra comment * tests/spin/pftp: commented out unused variable * bytecode.h, bytecode.c (bytecode_str_inf): added interface to query structure information. TODO: use binary search to find record. TODO: adapt interface for bytecode_src_loc 2006-03-14 Michael Weber * instr.c (instr_load_special_timeout): renamed to instr_lds_timeout (instr_load_special_pid): renamed to instr_lds_pid (instr_load_special_nrpr): renamed to instr_lds_nrpr (instr_load_special_last): renamed to instr_lds_last (instr_load_special_np): renamed to instr_lds_np (instr_lrun): fixed storage size bug (instr_run_intern): fixed storage size bug 2006-03-13 Michael Weber * Makefile (MACHINE): set MACHINE if compiler target architecture cannot be worked out from ``gcc -dumpmachine'', e.g. ``make MACHINE=x86_64-linux'' (CFLAGS): use -m64 for x86_64 (CFLAGS_LIB): use -fPIC by default on x86, except for win32 2006-03-11 Michael Weber * state.c (channel_to_str): more unsignedness fixes * instr.c (instr_chnew): more unsignedness fixes * hashtab.c (hashtab_get_pos): more unsignedness fixes * Makefile: changed way to detect mingw32 compiler to make it work with ming32 cross compiler, use -DSMALLSTACK by default in windows (TARGET): set TARGET to cross compile, e.g.: ``make TARGET=i586-mingw32msvc all'' * search.c: use #ifdef WIN32 ... #endif for windows specific sections * timeval.h: shift platform specifics here, just include if needed * instr_step.c: conditionalize on SMALLSTACK 2006-03-09 Michael Weber * hashtab.c (hashtab_hash): fixed signedness oversight 2006-02-23 Michael Weber * BUGS: Added Bug#2. * instr_step.c (instr_succ): extension of finite paths only if monitor is present. * state_inline.h (global_state_compare): add type cast so that C++ compilers don't choke. Note, that this function is deprecated, still. * nipsvm.h: comment cosmetics 2006-02-17 Michael Weber * nips_disasm.pl: very simple bytecode-to-C stub generator. The generated function must be inserted manually into the VM currently. Also, giving such a specialized VM a different bytecode file than was used for generating the C stub results in hilarious behavior. Not recommended. Speedup: yes, but not very large. Much is eaten by complicated PC handling. Possible optimizations: move instruction decoding out of execution loop (requires quite some surgery) * nips_asm_instr.pl (get_instructions): tag instructions whether they change control-flow or yield errors. (instruction_cfun): bytecode to C-function name mapping * instr.c (instr_ldc): renamed from instr_load_constant to match functions names generated by disassembler script (instr_trunc): renamed from instr_truncate (instr_exec): replaced occurrences of renamed functions 2006-02-15 Michael Weber * nips_asm.pl: collate flags for the same address instead of emitting them individually. Happens, if the compiler generates several labels for the same code address each of which has flags set. I am not sure that was a real problem for the current VM implementation. 2006-02-11 Michael Weber * state.c (global_state_to_str): output flags (accepting, terminated) if monitor is present 2006-02-06 Michael Weber * search.c (search_succ_cb): fixed type of succ_sz (size_t) * state.c (global_state_to_str): fixed format arg mismatch for 64-bit systems. 2006-02-03 Michael Weber * Released version 1.2.3 2006-02-02 Michael Weber * search.c (t_search_context, search, search_succ_cb): count transitions * nipsvm.h (nipsvm_state_monitor_accepting) (nipsvm_state_monitor_terminated) (nipsvm_state_monitor_acc_or_term): added * state.c, state.h (global_state_monitor_accepting) (global_state_monitor_terminated) (global_state_monitor_acc_or_term): deprecated 2006-02-01 Michael Weber * hashtab.c: faster hash collision resolution using (very simple) double hashing, speeding up almost-filled hash table insertions. I measured a speedup of 1.35 when filling hash table to 93%. API CHANGES AHEAD Old API functions are still there, but will be be phased out eventually. * nipsvm.c, nipsvm.h : beginnings of a new interface: nipsvm_* equivalents of the most used global_* methods * simpler and less fragile callback interface, all extra information is stashed away in nipsvm_transition_information_t (can be extended without visibly changing the API) * converted some of the internals to the new API (work in progress) * some state handling functions have grown an extra size_t argument, instead of calculating the state size themselves * search.c (search): added initial state to hash table to eliminate off-by-one difference between visited states and states in table * Makefile: added -g option by default, removed rt_err.o from libnips_vm (not needed) 2005-10-11, 2005-10-12 ---------------------- added range errors in assembler changed maximum size of global variables to 65535 - access to global variables 256..65535 not possible using LDVA / STVA use LDC
; LDV / STV instead added instructions - GLOBSZX set size of global variables using 2 byte constant - LDB [L|G] load bit from local / global memory stack:: ---> stack: only last 3 bits of are used - STB [L|G] store bit into local / global memory stack::: ---> stack must be 0 or 1 (other values are treated as 1) - LDV / STV [L|G] [2u|2s|4] LE load / store variable in little endian format works as version without LE at end (but in little endian format) - BGET /BSET r_i, b for bit access to registers behaviour is as FGET b / FSET b (but for r_i instead of r_F) 1.2.2 2005-09-30 ---------------- tried to fix unalign errors on alpha tried to fix left unalign errors on alpha fixed byte order bug in LVAR instructions (remote ref) added global_state_initial_size added string output of states 1.2.1 2005-09-21 ---------------- now forcing cycle in case of blocking system - needed in most LTL model checkers to recognize invalid states in which system blocks - added INSTR_SUCC_CB_FLAG_SYS_BLOCK flag (successor callback) 1.2 2005-09-06 -------------- first public release