DOC PREVIEW
Berkeley ELENG C249A - Timing-Based Communication Refinement for CFSMs

This preview shows page 1-2-19-20 out of 20 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 20 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 20 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 20 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 20 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 20 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Timing-Based Communication Refinement for CFSMsOutlineProblem DescriptionsRendezvous Based CommunicationOverviewSizing BuffersSlide 7Slide 8Clock HandlingBuffer ModelingReachable Buffer StatesMinimum Buffer SizeMixed HW/SW Implementation with CPU ContentionCPU ContentionSlide 15Slide 16Slide 17Issues: AbstractionIssues: Environment ModelingConclusionsTiming-Based Communication Refinement for CFSMsPresenters: Heloise Hse, Irene PoMentors: Jonathan Martin, Marco SgroiProfessor: Alberto Sangiovanni-VincentelliEE249 Course ProjectOutline•Problem descriptions•Rendezvous based communication•Buffer sizing•Mixed HW/SW implementation with CPU contention•Unresolved Issues•ConclusionProblem Descriptions•Currently, CFSM networks in Polis use one-place buffer•Non-blocking write•If sender CFSM module sends faster than receiver can receive, events may be overwritten / lostRendezvous Based Communication•Start with a rendezvous based specification–safe: events do not get lost–inefficient: senders have to wait until receivers are ready before sending more data•Relax to bounded buffers wherever possible–use minimal buffer sizes–maintain lossless communication–preserve input-output behaviorOverviewCFSM1 CFSM2CFSM3CFSM4FSM3FSM4FSM1 FSM2.........CFSM1 CFSM2CFSM3CFSM4.........Sizing Buffers•Translate each CFSM module into an FSM using translator in Polis•If state transition times are different, normalize the transition time by adding intermediate statesA EB C D102015102055A EBCDSizing Buffers•Model each buffer as a FSM•Compute the set of reachable states of the network from the transition relations using implicit state enumeration techniques R0 =  R k+1 = R0 V (x,i)[Rk T(x,i,y)] R* = Rk if R k+1 = Rk“Sizing and Verification of Communication Buffers for Communicating Processes” by Tilman Kolks, Bill Lin, and Hugo de ManSizing Buffers•Derive the set of reachable states for each communication buffer•Determine the minimum buffer size from the reachable states of the bufferClock Handling•Define a global “clock” (Gc) with frequency equal to the least common multiple of all frequencies fi (fi = clock frequency of FSM Fi)•A FSM makes a transition only when it is active original transition (i, s) -> s’ replace by (i  activei, s) -> s’ (i  ¬activei, s)->sBuffer Modeling•Model buffers as counters (FSMs)–start with an estimated size for each buffer –increment buffer on write, decrement on read•Initial buffer offset = 0•next state function: adder/subtracter•add an output function to the buffer Biiover = 1, iff an overflow condition occurs–expand the counters dynamically during state traversal when necessaryReachable Buffer States•Build transition relations for every FSM Fi and buffer Bk•Build the transition relation (TC) of the product machine over variables of the network•Obtain the reachable state set from TC•Expand the counters (buffers) dynamically during the state space traversal by adding an additional state variable if an overflow occursMinimum Buffer Size•Derive the set of all reachable buffers states by existentially quantifying over all non-buffer state variables•Derive the set of reachable states for a particular buffer by existentially quantifying (abstracting) out the other buffer states•Determine the minimum buffer size from the largest value of the counter stateMixed HW/SW Implementation with CPU Contention•If several processes are sharing a CPU, there may be contention due to resource sharing•Therefore we need to modify the buffer sizes to accommodate this caseSenderReceiverCPU Contention•Assume the CFSM network is a DAG and there are no feedback signals•To obtain safe minimum buffer size, assume–all the modules before and including the sender send at the fastest rate possible (i.e. get CPU right when it wants to execute)–receiver receives at the slowest rate (i.e. at end of queue every time it wants to execute)•Size buffer one at a timeHW/SWSW with CPU contection...CPU Contention•Build the reachable states table for processes that are sharing the same CPU•Assume scheduler is FIFO•For each state in an FSM–look at the possible states that other FSMs can be in, and put those processes in the front of the queue–Compute worst case waiting timeP1P2P3S1S2 S3S1S2S3’S1... ...CPU Contention•Compute worst case execution time (original execution time + worst case waiting time) and update the transition times in the original “FSM” •For each “FSM”, again normalize the transition time by adding intermediate states•Apply the buffer sizing algorithm on the normalized FSM’sCPU ContentionA EB C D20403020401010A EBCDIssues: Abstraction•State explosion problem during implicit state enumeration•One solution: abstracting away non-buffer variables during state traversal– may lose relevant information for buffer sizing when environment is control-dominated in which events depend on both time and value–need to abstract away variables in a smart wayIssues: Environment Modeling•In original buffer sizing algorithm, no assumption is made about the environment•Approach is very conservative and buffers may be oversized •Hard to model the environment•Possible solution: given all properties of the environment or test vectors of all possible input patterns, model the environment as an FSM, and then apply the algorithm in the paperConclusions•We presented an algorithm to find minimum-sized buffers between CFSM modules while maintaining lossless communication•The case of CPU contention has been


View Full Document

Berkeley ELENG C249A - Timing-Based Communication Refinement for CFSMs

Documents in this Course
Load more
Download Timing-Based Communication Refinement for CFSMs
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Timing-Based Communication Refinement for CFSMs and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Timing-Based Communication Refinement for CFSMs 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?