Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
C
cortex-m-rtfm-klee
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
KLEE
cortex-m-rtfm-klee
Commits
bac25a2a
Commit
bac25a2a
authored
Mar 11, 2018
by
Henrik Tjäder
Browse files
Options
Downloads
Patches
Plain Diff
Spellcheck and PEP8
parent
33a54b0f
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
gdb.py
+58
-44
58 additions, 44 deletions
gdb.py
with
58 additions
and
44 deletions
gdb.py
+
58
−
44
View file @
bac25a2a
...
@@ -147,7 +147,7 @@ def stop_event(evt):
...
@@ -147,7 +147,7 @@ def stop_event(evt):
try
:
try
:
ceiling
=
int
(
gdb
.
parse_and_eval
(
ceiling
=
int
(
gdb
.
parse_and_eval
(
"
ceiling
"
).
cast
(
gdb
.
lookup_type
(
'
u8
'
)))
"
ceiling
"
).
cast
(
gdb
.
lookup_type
(
'
u8
'
)))
except
:
except
gdb
.
error
:
print
(
"
No ceiling found, exciting!
"
)
print
(
"
No ceiling found, exciting!
"
)
sys
.
exit
(
1
)
sys
.
exit
(
1
)
...
@@ -167,13 +167,15 @@ def stop_event(evt):
...
@@ -167,13 +167,15 @@ def stop_event(evt):
elif
imm
==
3
:
elif
imm
==
3
:
if
debug
:
if
debug
:
print
(
"
Debug: found finish bkpt_3 at cycle {}
"
.
format
(
gdb_cyccnt_read
()))
print
(
"
Debug: found finish bkpt_3 at cycle {}
"
.
format
(
gdb_cyccnt_read
()))
gdb
.
post_event
(
Executor
(
"
si
"
))
gdb
.
post_event
(
Executor
(
"
si
"
))
elif
imm
==
4
:
elif
imm
==
4
:
if
debug
:
if
debug
:
print
(
"
Debug: found finish bkpt_4 at cycle {}
"
.
format
(
gdb_cyccnt_read
()))
print
(
"
Debug: found finish bkpt_4 at cycle {}
"
.
format
(
gdb_cyccnt_read
()))
gdb
.
post_event
(
posted_event_init
)
gdb
.
post_event
(
posted_event_init
)
...
@@ -204,7 +206,8 @@ def posted_event_init():
...
@@ -204,7 +206,8 @@ def posted_event_init():
else
:
else
:
if
debug
:
if
debug
:
print
(
"
Debug: Append Finish action at cycle {}
"
.
format
(
gdb_cyccnt_read
()))
print
(
"
Debug: Append Finish action at cycle {}
"
.
format
(
gdb_cyccnt_read
()))
outputdata
.
append
(
outputdata
.
append
(
[
file_name
,
task_name
,
gdb_cyccnt_read
(),
priority
,
"
Finish
"
])
[
file_name
,
task_name
,
gdb_cyccnt_read
(),
priority
,
"
Finish
"
])
...
@@ -411,7 +414,8 @@ def tasklist_get():
...
@@ -411,7 +414,8 @@ def tasklist_get():
for
line
in
fin
:
for
line
in
fin
:
# print(line)
# print(line)
if
not
line
==
"
// autogenerated file
\n
"
:
if
not
line
==
"
// autogenerated file
\n
"
:
return
[
x
.
strip
().
strip
(
"
[]
\"
"
).
split
(
'
'
)
for
x
in
line
.
split
(
'
,
'
)]
return
[
x
.
strip
().
strip
(
"
[]
\"
"
).
split
(
'
'
)
for
x
in
line
.
split
(
'
,
'
)]
"""
Run xargo for building
"""
"""
Run xargo for building
"""
...
@@ -420,8 +424,9 @@ def tasklist_get():
...
@@ -420,8 +424,9 @@ def tasklist_get():
def
xargo_run
(
mode
):
def
xargo_run
(
mode
):
if
"
klee
"
in
mode
:
if
"
klee
"
in
mode
:
xargo_cmd
=
(
"
xargo build --release --example
"
+
example_name
+
"
--features
"
+
xargo_cmd
=
(
"
xargo build --release --example
"
+
example_name
"
klee_mode --target x86_64-unknown-linux-gnu
"
)
+
"
--features
"
+
"
klee_mode --target x86_64-unknown-linux-gnu
"
)
elif
"
stm
"
in
mode
:
elif
"
stm
"
in
mode
:
xargo_cmd
=
(
"
xargo build --release --example
"
+
example_name
+
xargo_cmd
=
(
"
xargo build --release --example
"
+
example_name
+
"
--features
"
+
"
--features
"
+
...
@@ -447,7 +452,8 @@ def klee_run():
...
@@ -447,7 +452,8 @@ def klee_run():
bc_file
=
(
glob
.
glob
(
PWD
+
"
/
"
+
bc_file
=
(
glob
.
glob
(
PWD
+
"
/
"
+
klee_out_folder
+
klee_out_folder
+
'
*.bc
'
,
recursive
=
False
))[
-
1
].
split
(
'
/
'
)[
-
1
].
strip
(
'
\'
'
)
'
*.bc
'
,
recursive
=
False
))[
-
1
].
split
(
'
/
'
)[
-
1
].
strip
(
'
\'
'
)
if
debug
:
if
debug
:
print
(
PWD
+
"
/
"
+
klee_out_folder
)
print
(
PWD
+
"
/
"
+
klee_out_folder
)
print
(
bc_file
)
print
(
bc_file
)
...
@@ -493,8 +499,9 @@ def gdb_cyccnt_write(num):
...
@@ -493,8 +499,9 @@ def gdb_cyccnt_write(num):
def
gdb_bkpt_read
():
def
gdb_bkpt_read
():
# Read imm field of the current bkpt
# Read imm field of the current bkpt
try
:
try
:
return
int
(
gdb
.
execute
(
"
x/i $pc
"
,
False
,
True
).
split
(
"
bkpt
"
)[
1
].
strip
(
"
\t
"
).
strip
(
"
\n
"
),
0
)
return
int
(
gdb
.
execute
(
"
x/i $pc
"
,
False
,
True
).
except
:
split
(
"
bkpt
"
)[
1
].
strip
(
"
\t
"
).
strip
(
"
\n
"
),
0
)
except
gdb
.
error
:
if
debug
:
if
debug
:
print
(
"
Debug: It is not a bkpt so return 4
"
)
print
(
"
Debug: It is not a bkpt so return 4
"
)
return
4
return
4
...
@@ -631,7 +638,7 @@ gdb.execute("continue")
...
@@ -631,7 +638,7 @@ gdb.execute("continue")
# -'2' the threshold (ceiling 2) of X
# -'2' the threshold (ceiling 2) of X
# -'Enter' the 'Enter' event
# -'Enter' the 'Enter' event
#
#
# after 19 cycles we clam Y, raising treshold to 3
# after 19 cycles we clam Y, raising t
h
reshold to 3
# after 28 cycles we exit the Y claim, threshold 3 *before unlock Y*
# after 28 cycles we exit the Y claim, threshold 3 *before unlock Y*
# after 29 cycles we exit the X claim, threshold 2 *before unlock X*
# after 29 cycles we exit the X claim, threshold 2 *before unlock X*
# and finally we finish at 36 clock cycles
# and finally we finish at 36 clock cycles
...
@@ -651,7 +658,7 @@ gdb.execute("continue")
...
@@ -651,7 +658,7 @@ gdb.execute("continue")
# interarrival = [100, 30, 40]
# interarrival = [100, 30, 40]
# should match the arrival time of EXTI1, EXTI2, and EXTI3 respectively
# should match the arrival time of EXTI1, EXTI2, and EXTI3 respectively
# you may need to change the order depending or your klee/tasks.txt file
# you may need to change the order depending or your klee/tasks.txt file
# (in the future inter
r
arrival and deadlines will be in the RTFM model,
# (in the future interarrival and deadlines will be in the RTFM model,
# but for now we introduce them by hand)
# but for now we introduce them by hand)
#
#
# Implement function that takes output data and computes the CPU demand
# Implement function that takes output data and computes the CPU demand
...
@@ -670,8 +677,8 @@ gdb.execute("continue")
...
@@ -670,8 +677,8 @@ gdb.execute("continue")
# Looking up the WCETs from the `output_data`.
# Looking up the WCETs from the `output_data`.
# (It may be a good idea to make first pass and extract wcet per task)
# (It may be a good idea to make first pass and extract wcet per task)
##
##
# The total utili
liz
ation bound allows us to discard task sets that are
obviously illegal.debug
# The total utili
s
ation bound allows us to discard task sets that are
# (not the case here though)
#
obviously illegal.debug
(not the case here though)
#
#
# Assignment 3.
# Assignment 3.
#
#
...
@@ -681,27 +688,31 @@ gdb.execute("continue")
...
@@ -681,27 +688,31 @@ gdb.execute("continue")
# In general the response time is computed as.
# In general the response time is computed as.
# Ri = Ci + Bi + Ii
# Ri = Ci + Bi + Ii
# Ci the WCET of task i
# Ci the WCET of task i
# Bi the blockng time task i is exposed to
# Bi the block
i
ng time task i is exposed to
# Ii the interference (preemptions) task is exposed to
# Ii the interference (preemptions) task is exposed to
#
#
# where
# where
# Pi the priority of task i
# Pi the priority of task i
# Ai the inter
r
arval of task i
# Ai the interar
ri
val of task i
#
#
# We assign deadline = inter
r
arival and priorties inverse to deadline
# We assign deadline = intera
r
rival and prior
i
ties inverse to deadline
# (rate monotonic assignment, with fixed/static priorities)
# (rate monotonic assignment, with fixed/static priorities)
#
#
# Lets start by looking at EXTI2 whith the highest priority, so no interference (preemption)
# Lets start by looking at EXTI2 with the highest priority,
# so no interference (preemption)
# R_EXTI2 = 11 + B_EXTI2 + 0
# R_EXTI2 = 11 + B_EXTI2 + 0
#
#
# In general Bi is the max time of any lower priority task (EXIT1, EXTI3 in our case)
# In general Bi is the max time of any lower priority task
# holds a resource with a ceiling > Pi (ceileng >= 3 in this case)
# (EXTI1, EXTI3 in our case)
# holds a resource with a ceiling > Pi (ceiling >= 3 in this case)
# B_EXTI2 = 10 (EXTI1 holding Y for 10 cycles)
# B_EXTI2 = 10 (EXTI1 holding Y for 10 cycles)
#
#
# Notice 1, single blocking, we can only be blocked ONCE, so bound priority inversion
# Notice 1, single blocking, we can only be blocked ONCE,
# so bound priority inversion
#
#
# Notice 2, `output_data` does not hold info on WHAT exect resource is held
# Notice 2, `output_data` does not hold info on WHAT exact resource is held
# (merely each 'claim time at a specific ceiling'). However this is sufficient for the analysis.
# (merely each 'claim time at a specific ceiling').
# However this is sufficient for the analysis.
#
#
# so
# so
# R_EXTI2 = 11 + 10 = 21, well below our 30 cycle margin
# R_EXTI2 = 11 + 10 = 21, well below our 30 cycle margin
...
@@ -711,22 +722,24 @@ gdb.execute("continue")
...
@@ -711,22 +722,24 @@ gdb.execute("continue")
# where I_EXTI3 is the interference (preemptions)
# where I_EXTI3 is the interference (preemptions)
#
#
# Here we can undertake a simple approach to start out.
# Here we can undertake a simple approach to start out.
# Assume a deadline equal to our interarr
a
val (50)
# Assume a deadline equal to our interarr
i
val (50)
# I_EXTI3 is the sum of ALL preemptions until its deadlne.
# I_EXTI3 is the sum of ALL preemptions until its deadl
i
ne.
# in this case EXTI2 can preempt us 2 times (40/30 *rounded upwards*)
# in this case EXTI2 can preempt us 2 times (40/30 *rounded upwards*)
# I_EXTI3 = 2 * 11
# I_EXTI3 = 2 * 11
#
#
# The worst case blocking time is 15 (caused by the lower prio task EXTI1 holding X)
# The worst case blocking time is 15
# R_EXTI3 = 8 + 2 * 11 + 15 = 45, already here we see that EXTI2 may miss its deadline
# (caused by the lower prio task EXTI1 holding X)
# R_EXTI3 = 8 + 2 * 11 + 15 = 45, already here we see that
# EXTI2 may miss its deadline
#
#
# EXTI1 (our lowest prio task)
# EXTI1 (our lowest prio task)
# R_EXTI1 = C_EXTI1 + B_EXTI1 + I_EXTI1
# R_EXTI1 = C_EXTI1 + B_EXTI1 + I_EXTI1
#
#
# Here we cannot be blocked (as we have the lowest prio)
# Here we cannot be blocked (as we have the lowest prio)
# I_EXTI1 is the sum of preemptions from EXTI2 and EXTI3
# I_EXTI1 is the sum of preemptions from EXTI2 and EXTI3
# our deadline = interarr
av
ial is 100
# our deadline = interarri
v
al is 100
# we are exposed to 100/30 = 4 (rounded upwards) pree
p
mtions by EXTI2
# we are exposed to 100/30 = 4 (rounded upwards) preem
p
tions by EXTI2
# and 100/40 = 3 (rounded upwards) preempions by EXTI3
# and 100/40 = 3 (rounded upwards) preemp
t
ions by EXTI3
#
#
# I_EXTI1 = 37 + 4 * 11 + 3 * 8 = 105
# I_EXTI1 = 37 + 4 * 11 + 3 * 8 = 105
#
#
...
@@ -735,15 +748,15 @@ gdb.execute("continue")
...
@@ -735,15 +748,15 @@ gdb.execute("continue")
#
#
# Assignment 4.
# Assignment 4.
# Looking closer at 7.22 we see that its a recurrent equation.
# Looking closer at 7.22 we see that its a recurrent equation.
# Ri(0) indicating the inital value
# Ri(0) indicating the init
i
al value
# Ri(0) = Ci + Bi
# Ri(0) = Ci + Bi
# while
# while
# Ri(s) = Ci + Bi + sum ..(Ri(s-1))..
# Ri(s) = Ci + Bi + sum ..(Ri(s-1))..
# so Ri(1) is computed from Ri(0) and so forth,
# so Ri(1) is computed from Ri(0) and so forth,
# this requires a recursive or looping implmentation.
# this requires a recursive or looping impl
e
mentation.
#
#
# One can see that as initially setting a "busy period" to Ci+Bi
# One can see that as initially setting a "busy period" to Ci+Bi
# and compute a new (longer) "busy period" by taking into accout preemptions.
# and compute a new (longer) "busy period" by taking into accou
n
t preemptions.
#
#
# Termination:
# Termination:
# Either Ri(s) = Ri(s-1), we have a fixpoint and have the exact response time
# Either Ri(s) = Ri(s-1), we have a fixpoint and have the exact response time
...
@@ -754,8 +767,9 @@ gdb.execute("continue")
...
@@ -754,8 +767,9 @@ gdb.execute("continue")
# Notice, we have not dealt with the case where tasks have equal priorities
# Notice, we have not dealt with the case where tasks have equal priorities
# in theory this is not a problem (no special case needed)
# in theory this is not a problem (no special case needed)
#
#
# However, for exactly analysing the taskset as it would run on the real hardware
# However, for exactly analysing the taskset as it would run on the
# requires some (minor) modifications. *Not part of this assignment*
# real hardware requires some (minor) modifications.
# *Not part of this assignment*
#
#
# Examination for full score.
# Examination for full score.
# Make a git repo of your solution. (With reasonable comments)
# Make a git repo of your solution. (With reasonable comments)
...
@@ -765,14 +779,14 @@ gdb.execute("continue")
...
@@ -765,14 +779,14 @@ gdb.execute("continue")
# Print response times according to Assignment 3
# Print response times according to Assignment 3
# Print response times according to Assignment 4
# Print response times according to Assignment 4
#
#
# It should work with different assignments of the inter
r
arival vector.
# It should work with different assignments of the intera
r
rival vector.
# test it also for
# test it also for
# [100, 40, 50]
# [100, 40, 50]
# [80, 30, 40]
# [80, 30, 40]
# (Verify that your res
o
ults are correct by hand computations)
# (Verify that your results are correct by hand computations)
#
#
# Grading
# Grading
# For this part 1/3 of the exam 35 points
# For this part 1/3 of the exam 35 points
# Assignment 2, 10 points
# Assignment 2, 10 points
# Assi
n
gment 3, 10 points
# Assig
n
ment 3, 10 points
# Assi
n
gment 4, 15 points
# Assig
n
ment 4, 15 points
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment