99
1010 tracelock = lock()
1111
12- tracecapture(thread_id, call, args): # call is action name
12+ def tracecapture(thread_id, call, args): # call is action name
1313 tracelock.acquire()
1414 log(thread_id, call, "start", args) # log the call with arguments
1515 tracelock.release() # release here allows threads to interleave
4545For each API call in program, phases in order are: ready, start, call, finish
4646phase[thread] == start means thread holds tracelock to write call start
4747phase[thread] == finish means thread holds tracelock to write call finish
48- After processing last API call in its thread, phase[thread] == exit
48+ After processing last API call in its thread, phase[thread] == done
4949
5050log: contents of the tracelog written by all the threads
5151
6666program = (( 'listfiles' , ), # thread 0
6767 ( 'openfile' , )) # thread 1
6868
69- threads = range (len (program ))
69+ threads = range (len (program )) # one element of program for each thread
70+
71+ unsynchronized = False # False: use tracelock, True: ignore tracelock
7072
7173### State
7274
8183files = list () # filenames in filesystem
8284listing = list () # listfiles return value, FIXME ret should be in tracecapture
8385
86+ ### Safety condition
87+
88+ # phases where a thread can write to the log
89+ writing = ('start' ,'finish' )
90+
91+ def writing_threads ():
92+ """
93+ list of threads that can write to the log
94+ """
95+ return [ t for t in threads if phase [t ] in writing ]
96+
97+ def state_invariant ():
98+ """
99+ At most one thread can write to the log
100+ """
101+ return len (writing_threads ()) <= 1
102+
103+
104+ ### Other necessary functions
105+
106+ # run is allowed to stop
107+ def accepting ():
108+ return all ([ phase [t ] == 'done' for t in threads ])
109+
110+ # reset before another run
84111def reset ():
85112 global pc , phase , log
86113 pc = [ 0 for thread in program ]
87114 phase = [ 'ready' for thread in program ]
88115 log = []
89116 files = []
90117
91- reset ()
118+ ### Initialize
92119
93- def accepting ():
94- return all ([ phase [t ] == 'exit' for t in threads ])
120+ reset ()
95121
96122### Actions
97123
98124def start_enabled (thread ):
99125 return (phase [thread ] == 'ready'
100- and not [ t for t in threads if phase [t ] == 'start' ]) #lock is free
126+ and (not writing_threads () # lock is free
127+ or unsynchronized )) # ignore lock - might corrupt file
101128
102129def start (thread ):
103130 phase [thread ] = 'start' # acquire lock
104- log .append ((thread , program [thread ][pc [thread ]], 'start' )) # write log
131+ # write log, if it might be corrupted write 'XXX' at the end
132+ if state_invariant ():
133+ log .append ((thread , program [thread ][pc [thread ]], 'start' ))
134+ else :
135+ log .append ((thread , program [thread ][pc [thread ]], 'start' , 'XXX' ))
105136
106137def call_enabled (thread ):
107138 return phase [thread ] == 'start' # holding lock
@@ -110,46 +141,48 @@ def call(thread):
110141 global listing # we reassign whole list, we don't just update it
111142 phase [thread ] = 'call' # release lock, execute call
112143 action = program [thread ][pc [thread ]]
113- # FIXME should implement actions and handle them generically, hack for now
144+ # for now. handle each action in *program* as a special case inline here
114145 if action == 'openfile' :
115146 files .append ('file0' ) # only works if openfiles just called once
116147 if action == 'listfiles' :
117148 listing = copy (files ) # must copy now because open may change files
118149
119150def finish_enabled (thread ):
120151 return (phase [thread ] == 'call'
121- and not [ t for t in threads if phase [t ] == 'finish' ]) #lock is free
152+ and (not writing_threads () # lock is free
153+ or unsynchronized )) # ignore lock - might corrupt file
122154
123155def finish (thread ):
124156 phase [thread ] = 'finish' # acquire lock
125157 action = program [thread ][pc [thread ]]
126- # FIXME should handle actions generically, hack special cases for now
158+ # for now, handle each action in *program* as a special case inline here
127159 if action == 'openfile' :
128160 ret = files [- 1 ] # most recently appended
129161 if action == 'listfiles' :
130162 ret = listing # most recently appended
131- log .append ((thread , action , 'finish' , ret )) # write log
163+ # write log, if it might be corrupted write 'XXX' at the end
164+ if state_invariant ():
165+ log .append ((thread , action , 'finish' , ret ))
166+ else :
167+ log .append ((thread , action , 'finish' , ret , 'XXX' ))
132168
133- def release_enabled (thread ):
169+ def exit_enabled (thread ):
134170 return phase [thread ] == 'finish' # holding lock
135171
136- def release (thread ):
137- if pc [thread ] + 1 < len (program [thread ]): # more actions remain
138- phase [thread ] = 'ready' # release lock
139- pc [thread ] += 1 # advance to next action
140- else :
141- phase [thread ] = 'exit' # release lock, indicate done
172+ def exit (thread ):
173+ phase [thread ] = 'done' # release lock, indicate done
174+
142175
143176### Metadata
144177
145178state = ('pc' , 'phase' , 'log' , 'files' , 'listing' )
146179
147- actions = (start , call , finish , release )
180+ actions = (start , call , finish , exit )
148181
149182enablers = {start :(start_enabled ,), call :(call_enabled ,),
150- finish :(finish_enabled ,), release :( release_enabled ,)}
183+ finish :(finish_enabled ,), exit :( exit_enabled ,)}
151184
152185domains = { start : { 'thread' : threads },
153186 call : { 'thread' : threads },
154187 finish : { 'thread' : threads },
155- release : { 'thread' : threads }}
188+ exit : { 'thread' : threads }}
0 commit comments