联系方式

  • QQ:99515681
  • 邮箱:99515681@qq.com
  • 工作时间:8:00-21:00
  • 微信:codinghelp

您当前位置:首页 >> Java编程Java编程

日期:2021-12-01 09:25

CSC3333: Modelling Assignment

Aim

To gain experience in modelling, validation, and formal verification of a simple concurrent asynchronous

system.

Learning outcomes

This assignment will develop your knowledge and give you hands-on experience in:

? using Petri nets (in the form of Signal Transition Graphs) for modelling a concurrent system;

? using simulation to validate the model;

? using formal verification for detecting errors and increasing the confidence in the correctness of the

model;

? using software tools (Workcraft framework) for supporting the development process.

Deadline

*** 4pm on Thursday 9

th December 2021 ***

Weight

This assignment is worth 100% of the coursework mark for this module, i.e. 40% of the overall module

mark.

Assessment irregularities

This is an individual assignment, and the submitted models and report should be your own work (or

properly referenced). Do not share your work with other students to avoid facilitating plagiarism.

Multiway arbiters

The purpose of an N-way arbiter is to ensure mutually exclusive access to a shared resource used by N>1

clients. The ‘early release’ protocols of an N-way arbiter and a client are as follows.


Figure 1 - The ‘early release’ protocol of an N-way arbiter and the protocol of ith client.

Before accessing the resource, the i

th client sends a request to the arbiter (by raising signal ri). Such requests

can be sent concurrently by several clients. In response, the arbiter issues a grant (by raising signal gi).

Upon the receipt of the grant, a client can safely use the resource, with the guarantee that no interference

is possible from other clients. Having finished using the resource, the client lowers its request ri. At this

point the arbiter can issue a grant to another client, and concurrently lowers gi. Note that:

? It is guaranteed that at most one client can be in the critical section, i.e. the resource is used in a

mutually exclusive way.

? Even though it is possible that several of g1,…, gN are high simultaneously, it is guaranteed that all

but perhaps one clients to whom these grants have been issued have already indicated by lowering

their requests that they have exited their critical sections. In other words, at most one of the

Boolean expressions r1&g1,…,rN&gN can evaluate to 1, i.e. at most one client can be in its critical

section.

A stricter (a.k.a. ‘late release’), arbitration protocol requiring that at most one of g1,…, gN is high at any time

is shown in Figure 2. Note that any correct implementation of this protocol will be also a correct

implementation of the ‘early release’ protocol in Figure 1, and for the purposes of this assignment either

protocol is acceptable.

Figure 2 – Late-release arbitration protocol requiring that the grants are mutually exclusive. Note the

difference from the protocol in Figure 1(left).

ME element (a.k.a. mutex) is described in the lecture notes, and its protocol is shown in Figure 3.

Figure 3 - The mutex protocol.

A single mutex can arbitrate between two clients, i.e. it implements a 2-way arbiter following the ‘late

release’ protocol (and thus also the less strict ‘early release’ protocol in Figure 1(left)). For more than two

clients, several mutexes have to be combined using some logic gates. Consider the following interface, i.e.

names and types (input/output) of signals, of a basic cell (BC) for building multiway arbiters:

Figure 4 - The interface of a basic cell (BC) for building multiway arbiters.

Such a BC communicates with two clients using two 4-phase handshakes, r1/g1 and r2/g2. These

handshakes are initiated by clients. In particular, a BC must guarantee that at most one of the Boolean

expressions r1&g1 and r2&g2 can evaluate to 1, i.e. at most one of the clients is in its critical section. A BC

communicates also with its parent BC using the 4-phase r/g handshake. This handshake is initiated by the

BC itself, and the BC acts as a client from the point of view of its parent BC. Such an interface allows one to

implement multiway arbiters by building balanced binary trees with BCs as their nodes. Such a tree of BCs

must guarantee that the clients following the protocol in Figure 1(right) access their critical sections in a

mutually exclusive way, i.e. at most one of the Boolean expressions r1&g1,…,rN&gN can evaluate to 1; that is,

such a tree of BCs should implement the arbitration protocol in Figure 1(left) or Figure 2. Intuitively, it

represents a knockout tournament bracket

https://en.wikipedia.org/wiki/Tournament#Knockout_tournaments

where the arriving requests compete for the access to the resource. For example, an implementation of an

8-way arbiter as a balanced tree of BCs is shown below (in the root BC, the parent handshake is shortcircuited,

and so this BC can be replaced by a mutex as an optimisation).

Figure 5 - An 8-way arbiter built as a balanced tree of BCs.

Internally, BC must contain a mutex to cope with metastability associated with the arbitration between its

clients’ requests, and several logic gates. As a part of this assignment, you must formally specify the

behaviour of BC as an STG. You are not expected to derive a circuit implementation (if you do, it will not

be marked). Note that mistakes in a circuit can be extremely expensive in terms of the costs of recalling

various products (e.g. TV sets and mobile phones) deploying it, as well as huge reputational damage. Still

worse, the circuit may be deployed in a safety-critical system (e.g. an aircraft) where malfunction can result

in a loss of human lives. Hence, exhaustive verification is of paramount importance, and will be an

important part of assessment.

Tasks

1. Develop an executable formal model of BC in the form of a safe STG. The interface of BC must be as in

Figure 4, and the names of signals and their types (input or output) must be as shown.

2. Validate your model by simulation.

3. Formulate and formally verify relevant correctness properties of your model. Even simple

asynchronous systems may exhibit non-trivial behaviour, so make sure your verification strategy yields

high confidence in the correctness of your model.

4. Write a brief (strictly not more than 500 words) report describing how you approached the design,

validation, and verification, any problems you encountered / solved, and any other relevant findings. It

must also contain an image of your final model. (Optionally, it may contain 1 or 2 other images.

Verification properties formulated in REACH will not count towards the word limit, but their

explanations will.) This limit applies even if you do the advanced task below.

5. [Advanced] If you perform the above tasks well, it is realistic to get a mark in the II.1 region. If you aim

at a 1st class mark, your model should additionally solve the following problem. As explained in the

lecture notes, the mutex is vulnerable to unbounded delays associated with metastability resolution. In

a basic implementation of a multiway arbiter as a balanced tree of BCs, several metastability

resolutions occur sequentially – their number corresponds to the number of rounds in the tournament,

i.e. to the height of the tree. E.g. in the 8-way arbiter shown in Figure 5 the height of the tree is 3, so up

to 3 metastability resolutions take place sequentially, each having unbounded delay. This may result in

an unacceptably long response time of the arbiter as a whole. Re-design the BC so that no two

metastability resolutions in the whole tree happen sequentially, i.e. the response time of the arbiter is

no worse than the longest delay of a single metastability resolution that had to be performed, plus the

forward and backward signal propagation delays through the tree (which are not affected by

metastability and so are bounded). You must not modify the interface of BC or the way the tree of BCs

is constructed. Include a brief explanation of your ideas and an image of the final model (in addition to

the basic model) in the report. You should be able to reuse most of the verification strategy developed

for the basic model (so just state that in the report), but if you have any extra properties specific to this

design then you can include them too.

Submission

You should submit a single *.zip file to NESS by the above deadline. This file must contain:

? a Workcraft Signal Transition Graph (STG) models of:

o the basic model of a single BC, named “bc-basic.work”; and

o the advanced model of a single BC (a tree of such BCs would have concurrent metastability

resolution), named “bc-advanced.work”, if you have attempted the advanced part (note that

you still need to submit the basic model as well);

? a brief report in PDF format, named report.pdf (MS Word can save documents in PDF format).

Allocation of marks

The following indicative allocation of marks will be used for this assignment:

? Quality of the model [10 marks]

? Validation and formal verification [10 marks]

? Visual representation [4 marks]

? Report [6 marks]

? Concurrent metastability resolution [10 marks]

[Total 40 marks]

Notes and hints

? Avoid dummy transitions – they are not necessary for this model, have complicated semantics, and

some of the standard verification properties are limited to STGs without dummies.

? As the BC contains a mutex, there must be a mutex place in the STG. You may find it helpful to look at

the design of the CYCLE module in the online tutorial Hierarchical design of a realistic buck controller:

https://www.workcraft.org/tutorial/synthesis/decomposition/start

Generally, look at the online tutorials which we do during practicals – there is a lot of useful stuff there.

? The signals representing the mutex’s outputs (grants) should be internal (otherwise you will break the

interface of BC). Note that the above practical requires one to insert internal signals to correct the

phases of mutex's requests – in this assignment, the mutex's grants should be internal, and there is no

need to correct signal phases; so these two things are unrelated. Avoid using any other internal signals –

you are not expected to derive a circuit, so no need to detect/resolve CSC conflicts, etc.

? Workcraft can verify whether given signals follow the handshake protocol – this feature is

described in the Handshakes Verification tutorial:

https://workcraft.org/tutorial/method/handshake_verification/start

? Workcraft is a cutting-edge tool with frequent releases, so some of its functionality has not been

tested extensively. If you suspect a bug, don’t suffer in silence! In the past, some students got bonus

marks for quality bug reports which led to improvements in Workcraft. Please check first whether

you are using the last version of Workcraft and whether the issue was already reported on GitHub:

https://github.com/workcraft/workcraft/issues

Don’t forget to CC me in the bug reports, and I might ask you to show the problem during a practical if I

cannot reproduce it myself.

? Formal verification is very important for this assignment – to get a good mark you should go well

beyond the standard STG properties (explained in workcraft.org/help/verification). If your STG is buggy

you will lose marks in both “Quality of the model” (for making a mistake) and “Validation and formal

verification” (for poor verification strategy that failed to catch the bug) sections.

? Remember that the STG must be safe. If your STG is unsafe, the verification in Workcraft will not

work – you will usually get an error message with a violation trace exhibiting unsafeness – it could be

either a pop-up window or a message in the Output pane. One may try to synthesise a safe STG from an

unsafe but bounded one via Conversion→Net synthesis*** menu items. This will allow the verification to

proceed (though the mutex places are not always preserved by synthesis, so the choice between mutex

grants will cause violation of output-persistence), but may yield an incomprehensible STG.

? Your model should be visually comprehensible – nice layout, not messy, good use of node labels,

comments, good alignment of nodes, not too many crossing arcs, etc.

? For the report you will need to export images from Workcraft – this can be done is various graphics

formats via File→Export; in particular, SVG (vector graphics, so scales well) can be inserted into newer

versions of MS Word; PNG (raster graphics, so scales poorly) can be inserted into most text editors.

? The demonstrators are not expected to help you with this assignment – you should ask me (at a

practical or by email). I don’t normally answer questions like, “is this a correct way to model that?”,

“how to model that?”, “is this STG correct?”, “should I verify this property?” – these are related to the

modelling process and are a part of evaluation; the general advice is that you should capture in your

model the intended behaviour as well as possible, try to use the modelling techniques we considered in

the Petri nets part of the course, and think carefully about the verification strategy. However, I can

clarify the assignment spec if necessary, provide some general guidance concerning the intricacies of

Workcraft, the theory of Petri nets / STGs / circuits, etc., but without giving you any major spoilers.

If in doubt, just ask me – I may be able to help in some way, e.g. by pointing the relevant topics in the

lecture notes.


版权所有:编程辅导网 2021 All Rights Reserved 联系方式:QQ:99515681 微信:codinghelp 电子信箱:99515681@qq.com
免责声明:本站部分内容从网络整理而来,只供参考!如有版权问题可联系本站删除。 站长地图

python代写
微信客服:codinghelp