3 years agoSET: making SET configurable, adjust config model, cleanup 84/5684/2 master
Roman Sommer [Tue, 24 May 2016 12:46:21 +0000 (14:46 +0200)]
SET: making SET configurable, adjust config model, cleanup

This commit cleans up previous work. Code specific to Semi-Extended Tasks is now
placed inside corresponding ifdef blocks, also the config model has been
adjusted to not allow SET in conjunction with encoding and mpu support, which
both do not work in the current state.

Change-Id: Ie3dd4356461bd76d7db83bb6c5c71481970aad46

3 years agoMerge branch 'SET_i386'
Roman Sommer [Thu, 19 May 2016 12:44:34 +0000 (14:44 +0200)]
Merge branch 'SET_i386'


Change-Id: Ic1d7bde7a6a833be01536f56d0538148ded27f02

3 years agoSET: fixed.
Roman Sommer [Thu, 19 May 2016 11:58:47 +0000 (13:58 +0200)]
SET: fixed.
The problem was in the syscall wrappers. Because we may switch the stack before
a syscall, %esi was used to reference stack variables and LLVM consequently
ignored its presence in the clobber list. Adding push/pop %esi solved this.
Also sysenter_syscall may no longer (ever?) be "naked", because %ebp references
local variables and must be set to a valid value after entering

3 years agoimplemented SETs for i386 (still broken), working on fixing e.g. ecc1_eventisr1f
Roman Sommer [Fri, 13 May 2016 16:34:38 +0000 (18:34 +0200)]
implemented SETs for i386 (still broken), working on fixing e.g. ecc1_eventisr1f

3 years agoSET: prepare tcb for implementation of SET, reserve the 8 topmost bytes on ET stacks...
Roman Sommer [Fri, 13 May 2016 16:32:56 +0000 (18:32 +0200)]
SET: prepare tcb for implementation of SET, reserve the 8 topmost bytes on ET stacks for SET specific data (making basic_task_frame_pointer and is running valid entries in ETs); Note: only basic_task_frame_pointer is needed, but by saving space for both, BTs and (S)ETs behave the same way, which is much less confusing.

3 years agogenerator: add verify mockup stub 79/5679/2
Christian Dietrich [Thu, 12 May 2016 11:03:57 +0000 (13:03 +0200)]
generator: add verify mockup stub

The verify mockup stub can be activated generated a new build

    mkdir build
    cd build
    ../ -a posix --generate-mockup t

Change-Id: Ia980b9c3a1dd55df736484e2e58a5f2fad3612ca

3 years agosemi-extended-tasks: fix stack switch
Christian Dietrich [Fri, 22 Apr 2016 12:56:12 +0000 (14:56 +0200)]
semi-extended-tasks: fix stack switch

The stack switch of semi extended tasks was broken. This was mainly
caused by the missing Context save in _switchFromSETtoBT. There the
from->sp pointer was not set, therefore a TerminateTask in the Basic
Task caused an invalid start(old) call. All other changes in this patch
are mainly cosmetic.

3 years agomark-stack-switch: fix detection of subgraph roots
Christian Dietrich [Fri, 22 Apr 2016 12:51:12 +0000 (14:51 +0200)]
mark-stack-switch: fix detection of subgraph roots

3 years agorecreated conditions for segfault (set_anot1b)
Roman Sommer [Wed, 20 Apr 2016 13:33:20 +0000 (15:33 +0200)]
recreated conditions for segfault (set_anot1b)

3 years agorestored working state (set_anot1b)
Roman Sommer [Wed, 20 Apr 2016 13:32:03 +0000 (15:32 +0200)]
restored working state (set_anot1b)

3 years agoplaying with inlining, clobber lists and stack layouts
Roman Sommer [Fri, 1 Apr 2016 13:38:31 +0000 (15:38 +0200)]
playing with inlining, clobber lists and stack layouts

3 years agoposix/tcb.h: prepare merging of start(...) and switchTo(...)
Roman Sommer [Fri, 25 Mar 2016 23:44:12 +0000 (00:44 +0100)]
posix/tcb.h: prepare merging of start(...) and switchTo(...)

3 years agoposix/dispatch.h: removed unneeded case
Roman Sommer [Fri, 25 Mar 2016 23:28:18 +0000 (00:28 +0100)]
posix/dispatch.h: removed unneeded case

3 years agoposix/tcb.h: cosmetic changes to asm functions
Roman Sommer [Fri, 25 Mar 2016 23:19:04 +0000 (00:19 +0100)]
posix/tcb.h: cosmetic changes to asm functions

3 years agoposix/tcb.h: split off check for running on shared stack
Roman Sommer [Fri, 25 Mar 2016 23:12:24 +0000 (00:12 +0100)]
posix/tcb.h: split off check for running on shared stack

3 years agoposix/arch/{dispatch,tcb}.h: split off code for first dipatch
Roman Sommer [Fri, 25 Mar 2016 22:57:44 +0000 (23:57 +0100)]
posix/arch/{dispatch,tcb}.h: split off code for first dipatch

3 years agoposix/tcb.h: more cleanup, added ret instructions to asm functions
Roman Sommer [Thu, 24 Mar 2016 15:24:35 +0000 (16:24 +0100)]
posix/tcb.h: more cleanup, added ret instructions to asm functions

3 years agoposix/tcb.h: ongoing cleanup of switch_to_basic_task(...)
Roman Sommer [Thu, 24 Mar 2016 14:32:10 +0000 (15:32 +0100)]
posix/tcb.h: ongoing cleanup of switch_to_basic_task(...)

3 years agoposix/tcb.h: replaced common assembly sequences with macro
Roman Sommer [Thu, 24 Mar 2016 14:09:08 +0000 (15:09 +0100)]
posix/tcb.h: replaced common assembly sequences with macro

3 years ago{dispatch,tcb}.h: fix indent
Roman Sommer [Mon, 21 Mar 2016 14:37:10 +0000 (15:37 +0100)]
{dispatch,tcb}.h: fix indent

3 years agoAnalysis: Fix MarkStackSwitch pass
Stefan Bader [Tue, 15 Dec 2015 11:59:47 +0000 (12:59 +0100)]
Analysis: Fix MarkStackSwitch pass

Do not mark functions which call terminateTask() as stackSwitch-able

Change-Id: I112abe678eb4573df9b1154bc1b89feb851a9587

3 years agoStackSwitch testcases
Stefan Bader [Tue, 24 Nov 2015 14:14:13 +0000 (15:14 +0100)]
StackSwitch testcases

Change-Id: I70ce28dce111ee5d2bd7939e8587be6bfcdf8553

3 years agoadd AnotateStackSwitchFunction pass
Stefan Bader [Tue, 24 Nov 2015 13:48:35 +0000 (14:48 +0100)]
add AnotateStackSwitchFunction pass

This pass anotates the functions which can switch to stack in order to
implement semi extended tasks.
Fixed the indentation in arch/posix/tcb.h while i'm allready at it.

Change-Id: I1aef3947c047b177e4d26baeff89cc2515a719a5

3 years agoAnalysis: Fix MarkStackSwitch pass 61/5461/7
Stefan Bader [Tue, 15 Dec 2015 11:59:47 +0000 (12:59 +0100)]
Analysis: Fix MarkStackSwitch pass

Do not mark functions which call terminateTask() as stackSwitch-able

Change-Id: I112abe678eb4573df9b1154bc1b89feb851a9587

3 years agoStackSwitch testcases 57/5457/10
Stefan Bader [Tue, 24 Nov 2015 14:14:13 +0000 (15:14 +0100)]
StackSwitch testcases

Change-Id: I70ce28dce111ee5d2bd7939e8587be6bfcdf8553

3 years agoadd AnotateStackSwitchFunction pass 48/5448/9
Stefan Bader [Tue, 24 Nov 2015 13:48:35 +0000 (14:48 +0100)]
add AnotateStackSwitchFunction pass

This pass anotates the functions which can switch to stack in order to
implement semi extended tasks.
Fixed the indentation in arch/posix/tcb.h while i'm allready at it.

Change-Id: I1aef3947c047b177e4d26baeff89cc2515a719a5

3 years agoposix: Linker script groups data objects 65/5465/1
Christian Dietrich [Thu, 17 Dec 2015 15:24:44 +0000 (16:24 +0100)]
posix: Linker script groups data objects

The linker script for i386 does group the data objects into regions of

- OS Data (from &_sdata_os to &_edata_os)
  - Canonical OS Data  (&_sdata_canonical_os to &_edata_canonical_os)
- Arch Data (from &_sdata_arch to &_edata_arch)
  - Canonical Arch Data  (&_sdata_canonical_arch to &_edata_canonical_arch)

Change-Id: I72f43f7c0a42e714dc5a13a2db2e07a9f468f033

3 years agologging: fix handling of VERBOSE 64/5464/2
Christian Dietrich [Tue, 15 Dec 2015 15:57:09 +0000 (16:57 +0100)]
logging: fix handling of VERBOSE

Change-Id: I9dd66a450d2a697573a1406430626aaa219e78e3

3 years agogenerator/pass-manager: Fix order of oneof 63/5463/2
Christian Dietrich [Tue, 15 Dec 2015 15:55:42 +0000 (16:55 +0100)]
generator/pass-manager: Fix order of oneof

The oneof execution order was arbitrarily, triggering the bug from the
last commit. The oneof_tryall modifier was added to the pass information.

Change-Id: Ib725d67d8fb983395645c17366aeaf107793d237

3 years agogenerator/state-flow: fix collection of ISR states 62/5462/2
Christian Dietrich [Tue, 15 Dec 2015 15:54:06 +0000 (16:54 +0100)]
generator/state-flow: fix collection of ISR states

The intra isr states were not collected correctly. This influenced no
result, since it was always overriden by the execution of the symbolic
system execution. BUT, there was a bug in the pass manager that selected
one of both passes at random (set order) and revealed this bug.

Change-Id: I8f918930112d699338857da08fa6d427c2336f7a

3 years agogenerator: minor cleanups and refactorings 36/5436/5
Christian Dietrich [Wed, 25 Nov 2015 17:16:25 +0000 (18:16 +0100)]
generator: minor cleanups and refactorings

Change-Id: I6f2c928954e3a92ab678de01626a818835109ce4

3 years agogenerator: declarative pass information 35/5435/3
Christian Dietrich [Wed, 25 Nov 2015 15:56:29 +0000 (16:56 +0100)]
generator: declarative pass information

Provide a more declarative way to describe the general information about
a single pass. Tis might break stuff, I hope I got it right.

Change-Id: Ica35ca5f743c2bfa83ee8fc5d73a42515f39bf66

3 years agographs: fixup plotting of graphs 34/5434/3
Christian Dietrich [Wed, 25 Nov 2015 15:35:36 +0000 (16:35 +0100)]
graphs: fixup plotting of graphs

For the current graphs, graphviz does some times segfault. THIS IS A
KNOWN AND FIXED BUG. But it is not yet available in a release. Please
compile dot yourself.

Change-Id: I52c247c1cc8c46ee08668f3f9b04f077cc280325

3 years agoAnalysis: Add MarkStackSwitch pass 07/5407/11
Stefan Bader [Wed, 7 Oct 2015 13:41:20 +0000 (15:41 +0200)]
Analysis: Add MarkStackSwitch pass

Marks functions of extended Tasks which can switch
the stack.

Change-Id: Id74bd6c13f54bf0741ca3c28c1b07745ffbddd19

3 years agocmake: simplify build system 09/5409/1
Christian Dietrich [Fri, 23 Oct 2015 09:10:32 +0000 (11:10 +0200)]
cmake: simplify build system

remove some old cruft

Change-Id: Ie94b7dd352acec017979ce76fcc6d0f7fbd197b8

3 years agoBuild: Find "grub2-mkrescue" 08/5408/1
Stefan Bader [Tue, 20 Oct 2015 14:52:32 +0000 (16:52 +0200)]
Build: Find "grub2-mkrescue"

Prior to this cmake could only find "grub-mkrescue".

Change-Id: Id16ce4958d826953387c80865aafe47a5660eecd

3 years agofsm: change interrupt semantic 93/5393/1
Christian Dietrich [Tue, 22 Sep 2015 13:21:07 +0000 (15:21 +0200)]
fsm: change interrupt semantic

In the FSM representation, interrupts are no longer modled as separate

Change-Id: I3c9de5f629a5b36330e1339263700efabd34b822

3 years agoMerge remote-tracking branch 'gerrit/master' into encoded-event-fix
Christian Dietrich [Fri, 18 Sep 2015 13:48:08 +0000 (15:48 +0200)]
Merge remote-tracking branch 'gerrit/master' into encoded-event-fix

3 years agoContributor Agreement 82/5382/1
Christian Dietrich [Wed, 16 Sep 2015 13:34:42 +0000 (15:34 +0200)]
Contributor Agreement

Change-Id: If54efba52eed798bf95dda470f5b5bf714eb6f60

3 years agoi386: check saved_sp after usage
Christian Dietrich [Tue, 8 Sep 2015 08:08:16 +0000 (10:08 +0200)]
i386: check saved_sp after usage

Change-Id: Ic2554caf81492cb93b73c423a28fa014c6288ce5

3 years agox86: use popcnt for code generation
Christian Dietrich [Mon, 7 Sep 2015 14:43:11 +0000 (16:43 +0200)]
x86: use popcnt for code generation

We explicitly enable the popcnt instruction in the code generation stage.

Change-Id: I799aabebede13da1dae3adc0e8cd864b4bc817f6

3 years agoencoded/events: check calculated task priority before usage
Christian Dietrich [Mon, 7 Sep 2015 10:54:31 +0000 (12:54 +0200)]
encoded/events: check calculated task priority before usage

The priority of a task is caluclated from its dynamic-priority state
word and the event state words. Until now, we did not check this value
for being a correctly encoded value, which causes quite a number of SDCs
in the bench-coptermock-isorc numbers. Therefore, we check this value
for validity and hope for the best.

Change-Id: Ie95c1b64b56d79a6110455270fb099fee919269f

3 years agosse: do not wipe set events on SetEvent
Christian Dietrich [Mon, 7 Sep 2015 13:58:11 +0000 (15:58 +0200)]
sse: do not wipe set events on SetEvent

It is unwise to overwrite the set-event bitmask on a SetEvent system
call. ecc1_event1f will ensure the correct behavior in the future.

Change-Id: I98bf21664d381e6093c194ad0442ee168fc92764

4 years agoFixed typo in release type (staple -> stable) 53/5253/3
Martin Hoffmann [Thu, 28 May 2015 09:29:02 +0000 (11:29 +0200)]
Fixed typo in release type (staple -> stable)

Change-Id: I1d13300681efa07a74d2f82eef6a56f62e682fb1

4 years agoAdd total written and read os memory addresses to stats.dict 52/5352/3
Martin Hoffmann [Thu, 23 Jul 2015 15:15:56 +0000 (17:15 +0200)]
Add total written and read os memory addresses to stats.dict

Change-Id: I9a2790cf1dac9c068bd4ff98ae43d8bf9ba74613

4 years agoapp/bcc1/alarm3: make testcases less racy 55/5355/6
Christian Dietrich [Wed, 12 Aug 2015 07:39:06 +0000 (09:39 +0200)]
app/bcc1/alarm3: make testcases less racy

Somes these testcases produced


instead of


This is not a application or OS bug, but a race condition with the
waiting times.

Change-Id: I1e847e13188b15d567ce4efd92f473a4f39a666b

4 years agogenerator/SSE: alternative SSE with APP-FSM 54/5354/1
Christian Dietrich [Wed, 12 Aug 2015 07:18:36 +0000 (09:18 +0200)]
generator/SSE: alternative SSE with APP-FSM

The symbolic system execution is now able to enumerate all possible
system states with two different approaches. Either we can use the "old"
version which uses states with blocks to be executed in the next step,
like it is described in LCTES'15 (Dietrich et. al).

Or we can use the application finite state machines as basis. These
state machines are smaller (lesser nodes) than the application's
CFG. They are based on the task's ICFG.

Change-Id: I05e050ed3f39bd18ecf86b4d7bb423b4ce0825e0

4 years agogenerator: application FSM transformation 64/5264/2
Christian Dietrich [Mon, 8 Jun 2015 12:23:12 +0000 (14:23 +0200)]
generator: application FSM transformation

The ApplicationFSM pass transforms the ICFG of a task to a finite state
machine. This construction is done by transforming CFG-edges to
FSM-states, and CFG-blocks to FSM-transitions.

In a second step, the CFG-computation blocks are handled as FSM-epsilon
transitions. Then a standard epsilon elimination is done for

Change-Id: I874bc3b17ebaf16b58bb70226e5eef091e5cbbe9

4 years agoGenerator: add llvm function attribute modifier 44/5344/2
Stefan Bader [Tue, 4 Aug 2015 11:37:54 +0000 (13:37 +0200)]
Generator: add llvm function attribute modifier

Added a modifier for llvm bitcode files, which adds function attributes +
values to a specific function.

Change-Id: I57d71147c776686bfd18025d3090485b69da6bf8

4 years agostate-asserts: use color_assert again
Christian Dietrich [Mon, 27 Jul 2015 12:18:32 +0000 (14:18 +0200)]
state-asserts: use color_assert again

Change-Id: Iebb4498dcb5c8a1ebb6bae8d13b75e4645e1cba6

4 years agoasserts: return to shortcutting semantic of state-asserts
Christian Dietrich [Mon, 27 Jul 2015 11:09:14 +0000 (13:09 +0200)]
asserts: return to shortcutting semantic of state-asserts

Change-Id: I38d53965e1dfe1c337a946bc7d47239a62a5cd3e

4 years agoscheduler: dispatchToCurrentTask should be inlined
Christian Dietrich [Mon, 27 Jul 2015 08:10:56 +0000 (10:10 +0200)]
scheduler: dispatchToCurrentTask should be inlined

Change-Id: I14a18026ef4e6320dd0c6da61fb8f6c4892ca16f

4 years agocfg-regions: delete all unused bits after check
Christian Dietrich [Mon, 27 Jul 2015 08:10:06 +0000 (10:10 +0200)]
cfg-regions: delete all unused bits after check

Not all bits in the cfg region word are used, therefore we can safely
reset them so a known state afterwards.

Change-Id: Ic059b80bf46f9a53742383025e495e653837cb68

4 years agofail: expose --inline-scheduler in variant name 25/5325/1
Christian Dietrich [Thu, 23 Jul 2015 14:50:01 +0000 (16:50 +0200)]
fail: expose --inline-scheduler in variant name

Change-Id: I83cac7005d667bdfd2045f8e0e58c03bddf1a475

4 years agoos/scheduler: make schedule inlinable again 20/5320/3
Christian Dietrich [Mon, 20 Jul 2015 16:11:32 +0000 (18:11 +0200)]
os/scheduler: make schedule inlinable again

Inlining the scheduler reveals a high potential for specialization and
and SDC reduction. In the implementation of the zedboard benchmark, we
dropped the inlinability support. This is now possible again. With
inline-scheduler+specialization the scheduler is paritally instansiated
whereever possible.

Test-Config: --arch i386 --encoded=no --inline-scheduler=yes --specialize=yes
Test-Config: --arch i386 --encoded=no --inline-scheduler=yes --specialize=no
Test-Config: --arch i386 --encoded=no --inline-scheduler=no --specialize=yes
Test-Config: --arch i386 --encoded=no --inline-scheduler=no --specialize=no
Test-Config: --arch i386 --encoded=yes --inline-scheduler=yes --specialize=yes
Test-Config: --arch i386 --encoded=yes --inline-scheduler=yes --specialize=no
Test-Config: --arch i386 --encoded=yes --inline-scheduler=no --specialize=yes
Test-Config: --arch i386 --encoded=yes --inline-scheduler=no --specialize=no

Change-Id: I2749078a3cc4ebeeb19bde14eb769b5781ac409f

4 years agobuild system: proper inlining 24/5324/1
Christian Dietrich [Thu, 23 Jul 2015 10:53:21 +0000 (12:53 +0200)]
build system: proper inlining

Inlining is hard. Convincing the compiler to actually inline the
systemcall bodies is even harder. Therefore we now use the always_inline
flag together with the -always-inline (llvm-opt) compiler
pass. Furthermore -gc-section drops all unused functions.

Change-Id: Ifd429e28ebb330944230076bca3886f4ef1171e3

4 years agoos/scheduler: unify 19/5319/1
Christian Dietrich [Mon, 20 Jul 2015 13:38:44 +0000 (15:38 +0200)]
os/scheduler: unify

Until know there where two different versions of, one for
encoded and one for the unencoded variant. In essence they were nearly
identical. Therefore, they could be unified without changing the
execution sequence.

Change-Id: Ifff4cd4a18bee135e286f330212aa14247cc2277

4 years agoi386: FaultDetectedHook in page fault handler 60/5260/2
Christian Dietrich [Fri, 29 May 2015 19:00:09 +0000 (21:00 +0200)]
i386: FaultDetectedHook in page fault handler

Like the last change, this one does not change the SDC rate, but does only make
them detectable by application/FAIL*. Until now, MPU faults were routed to isr_undetected

Change-Id: Iac81f8611753cafbddb6d1f9c4bbe505a788890e

4 years agoi386: FaultDetectedHook on unhandled interrupt 59/5259/2
Christian Dietrich [Fri, 29 May 2015 17:11:41 +0000 (19:11 +0200)]
i386: FaultDetectedHook on unhandled interrupt

Until now, unhandled interrupt resulted in a hanging machine. This did *not*
cause the SDC rates to change, but made the TIMEOUT numbers for fault injection
campaigns slightly too high.

Change-Id: I4616c5ddad66659bab604cd3ed5b5405ceea44ce

4 years agotrace analysis: Adding info for accessed OS memory 57/5257/3
Martin Hoffmann [Fri, 29 May 2015 11:04:26 +0000 (13:04 +0200)]
trace analysis: Adding info for accessed OS memory

This includes using nm again, instead of llvm-nm.

Change-Id: Ic8b1b6054427ddaf028ece5e7758309ee0d4b3be

4 years agofail: fix workspace check script 58/5258/1
Christian Dietrich [Fri, 29 May 2015 14:06:07 +0000 (16:06 +0200)]
fail: fix workspace check script

Change-Id: Ia516171592bc51c9fcef37fa9d2f2c9e947dd148

4 years agofail: simplify scripts 56/5256/2
Christian Dietrich [Thu, 28 May 2015 08:41:34 +0000 (10:41 +0200)]
fail: simplify scripts

Change-Id: I5303f2cd78122dd07921a97c5a598254bc3915fd

4 years agobenchmark-isorc: remove doubled priority 55/5255/2
Christian Dietrich [Thu, 28 May 2015 08:14:42 +0000 (10:14 +0200)]
benchmark-isorc: remove doubled priority

Change-Id: I35c6ef1c68bbcc016602b7ee70dd41a48a8a4087

4 years agoi386: Add noreturn to Machine:unreachable. 52/5252/1
Martin Hoffmann [Thu, 28 May 2015 08:52:24 +0000 (10:52 +0200)]
i386: Add noreturn to Machine:unreachable.

unreachable should not, and does not return.
This also silences a compiler warning.
Uses new C++11 attribute syntax [[noreturn]].

Change-Id: Ifb4438bffb6d6df641003c53d3a2bf4a825b403c

4 years agox86: make privilege isolation optional 46/5246/3
Christian Dietrich [Wed, 20 May 2015 14:14:35 +0000 (16:14 +0200)]
x86: make privilege isolation optional

Since privilege isolation is a very costly feature, and we're not sure
wheter it is good or bad for dependability, we make it optional. This
allows us to evaluate it separately.

Test-Config: --arch i386 --privilege-isolation f
Test-Config: --arch i386 --privilege-isolation f --mpu t
Test-Config: --arch i386 --privilege-isolation f --encoded t
Test-Config: --arch i386 --privilege-isolation f --basic-tasks t
Change-Id: Ia22a41eb610b090aeaac486d006a4b4ea2ab762a

4 years agox86/idt.S: Remove unecessary push 45/5245/1
Christian Dietrich [Thu, 21 May 2015 13:20:13 +0000 (15:20 +0200)]
x86/idt.S: Remove unecessary push

The push %edi was totally unecessary.

Change-Id: I4fc8806c722a1690f6a83678c35aa508ee64c3cf

4 years agoi386: All MMU related functions can be disabled 43/5243/3
Christian Dietrich [Wed, 20 May 2015 13:10:47 +0000 (15:10 +0200)]
i386: All MMU related functions can be disabled

All MMU related datastructres are now removed from the image, if dOSEK
is build without MPU.

Change-Id: If01c87027df73b92f3df979d0955098c4b5c91c3

4 years agofail/test.h: remove disable interrupt 44/5244/1
Christian Dietrich [Wed, 20 May 2015 14:23:44 +0000 (16:23 +0200)]
fail/test.h: remove disable interrupt

The disable interrupts at that place, caused the bench-coptermock to break.

Change-Id: Iedea2a6c259e276c3101dc8970ff29a2e1b57e9a

4 years agoPreciseSystemState: memory efficient variant 42/5242/2
Christian Dietrich [Tue, 19 May 2015 14:47:13 +0000 (16:47 +0200)]
PreciseSystemState: memory efficient variant

We implement the PreciseSystemState with a more efficient variant. It
uses the __slot__ feature of python (therefore I removed it from the
inheritance chain, which causes some copying of code).

With this change the memory consumption for bench-coptermock drops from
~60Mb to ~40Mb for the SymbolicSystemExecution pass. With pypy3, the
memory consumption drops to 23Mbyte.

Change-Id: Ic87be8afa97d6861dfe49c9cffd40d3bdc6464a5

4 years agoextractor: separate executable for llvm 41/5241/1
Christian Dietrich [Tue, 19 May 2015 13:11:57 +0000 (15:11 +0200)]
extractor: separate executable for llvm

In order drop our dependency on llvmpy, which seems to be abandoned at
the moment, I implemented the llvm-extractor tool. It:

- splits basic blocks before and after each CallInst/InvokeInst
- rename the system calls
- extracts the system call arguments
- dumps a python dict with the strucutre

Change-Id: I2adac08c14ceb2e49ffe1bbcb43216b6769b06c1

4 years agobenchmark: port the coptermock benchmark from the ISORC'13 paper 35/5235/3
Christian Dietrich [Thu, 7 May 2015 08:24:27 +0000 (10:24 +0200)]
benchmark: port the coptermock benchmark from the ISORC'13 paper

In order to port the "old" isorc benchmark, I had to adapt the code only
a little bit to work around the constant-referencing of system objects
pollicy of dOSEK. Facts about the benchmark are:

- If run at 50Mhz
  - Takes 1.3 seconds (The original ISOR benchmark took 1.29 seconds)
  - Emits 110 checkpoints
    - Original CiAO: 107 (almost no diff to the current trace)
    - Original eCOS: 110 (two execution blocks are shuffled)

Change-Id: I6ab96fae29e1c8376da95ec4f622dc1d92843f4d

4 years agogenerator: Implement GetEvent systemcall 34/5234/3
Christian Dietrich [Thu, 7 May 2015 08:21:16 +0000 (10:21 +0200)]
generator: Implement GetEvent systemcall

The system call was already implemented in the scheduler API, but was
not exposed to the applications.

Change-Id: I08206e0a5e83011b63efb8257c1a57c00a93a8ba

4 years agofail: fix trace-analyze 33/5233/3
Christian Dietrich [Thu, 7 May 2015 08:04:42 +0000 (10:04 +0200)]
fail: fix trace-analyze did crash on the current traces due to a API change in
stats_binary. Additionally syscall_end markers are now also detected as
end of system-call--regions markers.

Change-Id: I2d9c09d235a6c2afda34d2b6aace86665b39d2b2

4 years agofail: Fix generation of variant name 36/5236/1
Christian Dietrich [Thu, 7 May 2015 15:24:45 +0000 (17:24 +0200)]
fail: Fix generation of variant name

Change-Id: Ic573cdf0d03f55fd523007127c15a0480ef436c8

4 years agodispatcher: rename ::idle to ::Idle 19/5219/1
Christian Dietrich [Wed, 6 May 2015 07:36:43 +0000 (09:36 +0200)]
dispatcher: rename ::idle to ::Idle

With this name change all upper case function from the dispatcher start
with an uppercase letter

Change-Id: I916a11094861c95cc179888090e1ff3d681c021d

4 years agoi386/qemu: use -kernel instead of -cdrom 18/5218/1
Christian Dietrich [Wed, 6 May 2015 07:29:05 +0000 (09:29 +0200)]
i386/qemu: use -kernel instead of -cdrom

Change-Id: Iaba3e4663749312b432c49c59c37e6fb2b62b116

4 years agowhitespaces: remove spurious whitespaces 17/5217/1
Christian Dietrich [Wed, 6 May 2015 07:18:25 +0000 (09:18 +0200)]
whitespaces: remove spurious whitespaces

Change-Id: I21d06ffc334fcb349f657023cc52ba63d756d3df

4 years agobasic tasks: implement basic tasks for x86 16/5216/1
Christian Dietrich [Wed, 6 May 2015 07:05:58 +0000 (09:05 +0200)]
basic tasks: implement basic tasks for x86

Basic tasks are quite easy on x86. Some essential bits of knowledge here

- since we always execute the kernel on a distinguished
  stack (event-based kernel), we always have a save returnable context
  on the user stack.
- As always we need a basic task frame pointer (BTFP) to remove the basic
  task's stack segment from the shared stack.
- We HAVE to to the BTFP fiddling in the dispatching interrupt, since
  our i386 variant is interruptible (will break at bcc1_lukas_alarmstress!)

Change-Id: I07b5e376cf29ba45d48f210cc2ab5cbac57888fa

4 years agoconfig: make idle halt part of the model 15/5215/2
Christian Dietrich [Tue, 5 May 2015 12:09:25 +0000 (14:09 +0200)]
config: make idle halt part of the model

Change-Id: I65ef8faed327fb01b00a4cc6538aa13f155efab5

4 years agospecialized: give information about old task on dispatch is available 14/5214/2
Christian Dietrich [Thu, 30 Apr 2015 16:05:38 +0000 (18:05 +0200)]
specialized: give information about old task on dispatch is available

With information about the previous running task, we can achieve better
code generation for dispatching of basic tasks. Until now this is only
implemented for posix.

Change-Id: Ic78142bed34cba0ffe69c5d0895547cbc48331b7

4 years agobasic tasks: Implementation for posix 93/5193/3
Christian Dietrich [Mon, 27 Apr 2015 09:23:26 +0000 (11:23 +0200)]
basic tasks: Implementation for posix

Basic tasks are a little bit complicated to implement. If we allow basic
tasks to run on a shared stack, we have to ensure that the stack is
switched correctly for all combinations of BT->ET, ET->BT, BT->BT task
switches. The testcases in app/ecc1/bt1 hopefully ensure the correct

Change-Id: I35ad89e0d02b83383cc6637b65be283a7436a2bc

4 years agofail: fix import arguments
Christian Dietrich [Wed, 29 Apr 2015 16:14:52 +0000 (18:14 +0200)]
fail: fix import arguments

4 years agocmake: small cleanup of unused rules 92/5192/1
Christian Dietrich [Wed, 29 Apr 2015 11:46:14 +0000 (13:46 +0200)]
cmake: small cleanup of unused rules

Change-Id: I5df36a0f65995a4024fbdc0c875af4f5605236ec

4 years agoconfig: distributed constraints 84/5184/4
Christian Dietrich [Thu, 23 Apr 2015 12:15:43 +0000 (14:15 +0200)]
config: distributed constraints

constraints on the configuration can now be cluttered over the whole
(python) source code. The constraints are at the moment checked at
configuration time of the system, and not in every generator call.

As an example, you can now use

 config-constraint-: dependability.state-asserts -> (os.systemcalls == normal)

All constraints are started with `config-constraint-:'. The constraint
can be continued to the following line with ':-:'. For example,

  config-constraint-: os.specialize ->
               :-:      (arch.self == ARM)

Change-Id: I84dda39ccaa862b9dc7d4b2b53fe205ee2b8f93e

4 years agoconfig: use config system in generator and code 83/5183/5
Christian Dietrich [Wed, 22 Apr 2015 12:12:35 +0000 (14:12 +0200)]
config: use config system in generator and code

Use the configuration values in the code (forced include) and within the
generator itself. This needed some adaptions to the code.

Change-Id: Iad330f2dd0af39c33ba753b5592b4df4c61974e7

4 years agoconfig: configuration system in 82/5182/2
Christian Dietrich [Wed, 22 Apr 2015 10:53:33 +0000 (12:53 +0200)]
config: configuration system in

The new configuration system uses a explicitly defined hierarchical
model. At the moment, this model is not checked against any
constraints. Nevertheless, the command line interface for and generator/ are already constructed in a
large extend from the model.

The current configuration model can be found in config/

Change-Id: I80464a2b5b3926da6e79603f586cb3df31409881

4 years agoState Replicator: bugfix, and enhanced fault detection propagation 16/4716/3
Martin Hoffmann [Fri, 19 Dec 2014 10:52:57 +0000 (11:52 +0100)]
State Replicator: bugfix, and enhanced fault detection propagation

towards first Fail* tests.

Change-Id: Ib5bce844b89fa046e84ee74651b81060db8552bc

4 years agotoolchain: Invoke toolchain with cross compiler 53/4453/7
Martin Hoffmann [Mon, 20 Apr 2015 07:33:31 +0000 (09:33 +0200)]
toolchain: Invoke toolchain with cross compiler

We actually need a cross compiler setup, even for the i386 variant.
This change invokes the i386-elf- toolchain.
(It only worked in Linux, as it uses the same ELF format for executables)

The corresponding tools (nm, objdump) are propagated to the various
scripts and builds.

Fixes for Linux variant.
Fixes for posix variant.
Use /proj/i4danceos/tools/llvm-3.4 as Hint

Change-Id: I46b9dcdb5e0292b4083a0a6456384ef71f8ebe31

4 years agozedboard-mm: matrix multiplication application for zedboard 88/5188/1
Christian Dietrich [Mon, 27 Apr 2015 13:27:08 +0000 (15:27 +0200)]
zedboard-mm: matrix multiplication application for zedboard

This application is no OSEK application, but uses dOSEK only as a boot

Change-Id: Ie05bb6a1ffc66ce32f800a5bc3c6ce3b767e78e3

4 years agoarm: use idle halt 78/5178/1
Christian Dietrich [Fri, 17 Apr 2015 07:53:47 +0000 (09:53 +0200)]
arm: use idle halt

The ARM port used a busy idle loop until now

Change-Id: I5d13b1f3cdcb998f62a72a45ac0c2cf1863f1ee7

4 years agoarch/posix: use virtual time for timers 92/4192/8
Florian Lukas [Fri, 4 Apr 2014 10:11:10 +0000 (12:11 +0200)]
arch/posix: use virtual time for timers

Virtual instead of real timer is used for timers to increase determinism.
The delay in the alarm3/ testcases had to be increased as a result, as
the virtual time progresses slower.

Change-Id: I61fabb8e8c869c7f5e3f078f961882abba2578c3

4 years agoAdd a Changelog v1.1
Christian Dietrich [Wed, 1 Apr 2015 12:41:26 +0000 (14:41 +0200)]
Add a Changelog

Change-Id: Ifeac07ba9a401ae011ac8fa15ee5819aa9b9c5f8

4 years agogenerator: syscall FSM/PLA implementation 05/5105/1
Christian Dietrich [Fri, 20 Mar 2015 16:29:45 +0000 (17:29 +0100)]
generator: syscall FSM/PLA implementation

Implement all system calls as PLA implementations.

Change-Id: I1f0bdcdc085727f5ce7e0aa6e6d83db87ae4896a

4 years agogenerator: LogicMinimizer for FSM Truth Table 04/5104/1
Christian Dietrich [Fri, 20 Mar 2015 15:16:52 +0000 (16:16 +0100)]
generator: LogicMinimizer for FSM Truth Table

We assign optimal state names for a two level PLA table. We use the
`nova' tool for the state assignment, which uses `espresso' logic
minimizer in the background.

Change-Id: Iefcff366ca5dc252cc23c8aacdc20954e13d0cce

4 years agogenerator/fsm: proper renaming of all components 80/5080/1
Christian Dietrich [Thu, 19 Mar 2015 11:40:46 +0000 (12:40 +0100)]
generator/fsm: proper renaming of all components

During the usage of the FiniteStateMachine, we will constantly rename
state, action, and event labels.

Change-Id: Ic255bb3b256ef4b8a41b501c6f5c3dae924bb37c

4 years agogenerator: Smaller SimpleFSM implementation 79/5079/4
Christian Dietrich [Thu, 19 Mar 2015 08:52:39 +0000 (09:52 +0100)]
generator: Smaller SimpleFSM implementation

The SimpleFSM implementtion does now use a dispatching table.

Change-Id: Ibe685e921801a148365868e8e99427f9e00e76b6

4 years agogenerator: oil reading and llvmpy reading as passes 77/5077/2
Christian Dietrich [Wed, 18 Mar 2015 14:24:47 +0000 (15:24 +0100)]
generator: oil reading and llvmpy reading as passes

Reading the OIL file and the llvmpy basic blocks is done in
passes. Therefore, we can omit them in the future, if wanted.

Change-Id: Ideef98fc1d9a74af498c522b1509a9d9f2289c92

4 years agogenerator: big refactoring 76/5076/4
Christian Dietrich [Wed, 18 Mar 2015 09:57:50 +0000 (10:57 +0100)]
generator: big refactoring

Rename all parts in a more logical way. The generator is now divided
into three main parts:
  - analysis: Generate GCFG and State Transition graph
  - transform: Generate Assertions, CFG Regions, FSMs
  - coder: bring the information collected in the previous steps down to
           the code.

Change-Id: I5cfd48f6a8d195c30b16b425eda010d9b0405dcd

4 years agoFSM: Minimize the state machine 74/5074/1
Christian Dietrich [Tue, 17 Mar 2015 13:04:38 +0000 (14:04 +0100)]
FSM: Minimize the state machine

The state machine we have developed until now is very redundant. We can
get rid of most of the states, by normal DFA minimization. We declare
two states to be in the same equivalence class, if they produce the same
dispatch sequence for all events.

Change-Id: Ic9dc330acb61597715c9876e138d57a9b8a3cc69

4 years agokeso: update the transformed gc_coffebreak sources 73/5073/1
Christian Dietrich [Tue, 17 Mar 2015 16:22:47 +0000 (17:22 +0100)]
keso: update the transformed gc_coffebreak sources

Change-Id: I06b49fd63adc87f0c7a57cc0dbfa5b2e948f423d