In this class, we will consider how serial, sequential programs are specified and how the correctness of their implementations is confirmed. This class will require careful thought as we will be pushing the boundaries of what the academic community considers to be an adequate specification and sufficient confirmation evidence that a program meets its specification. Typically, some form of testing is the only mechanism that is used to see if a program meets its specification -- this class will investigate both testing and other methods.
To be able to debug programs, we will investigate common debugging and analysis tools. To be able to use such tools effectively, it will be necessary for students to understand how binary is used to direct a processor. Students will need to understand how binary programs are organized and also how to inspect such binary programs during their execution.
Another component of debug and verification is a well-organized method for program development. Version control for code and documentation is widely used and is generally necessary -- especially in multi-person teams.
In some cases, we will use proof-based techniques to determine the correctness of our code. At first, we will investigate hand proofs; that is, we will use some informal notation to compare a specification program to an implementation program. We will also convert the behavior of some programs into a form that will allow a mechanical comparison of the behavior of two programs.
This class will be taught in an "inverted" style. That is, we will concentrate class time on examples, working through code, describing challenges, and exploring problems being faced by students. Thus, it is important that you bring your laptop to class. There will be lectures to introduce various topics, but primarily, we will use class time for problem solving, demonstrating how to use various tools, and exchanging information.
We will sometimes refer to your CS429 textbook ("Computer Systems, A Programmer's Perspective" by Randal E. Bryant and David O'Hallaron, Prentice Hall). We will make use of the second edition of the book "Hacker's Delight" by Henry S. Warren, Jr. This book will be used for various background problems, and some of the homework and programming assignments will be based on the material in this book. We will make use of other web-based material. There is a website associated with the "Hacker's Delight" book. And a great source of problems is the Hakmem website.
Tests and quizzes are open-book, open-notes affairs -- however, no electronic devices (laptops, cell phones, tablets, PDAs, calculators, etc.) of any kind are allowed during test and quiz events. As such, you may wish to have a physical copy of any materials that you believe will be helpful during quizzes and exams. Certainly, you should bring the "Hacker's Delight, Second Edition" class textbook; it will be helpful when taking quizzes and exams. Remember, cell phones are not allowed during exams; during quizzes and exams the remaining time will be periodically announced.
This course requires students to program in C. Knowledge of assembler will also be critical as it is the binary code that really determines what programs do -- and it is during binary execution that code will fail. It is recommended that you have access to "The C Programming Language", Second Edition, by Brian Kernighan and Dennis Ritchie, Prentice Hall Software Series. For examples and help with C-language use, you will find that there are many Web pages devoted to C-language programming.
Why C, or its extension, C++? It is the language that is used to implement many systems, such as FreeBSD, Linux, MacOS, Windows, as well as many user tools (e.g., wc, grep, ed, sed, emacs,...). Java programmers should have no problem with the subset of C that we will use, but Java programs will not be used to interface with assembly language programs. Students will be introduced to some C-language capabilities, such as referencing x86 processor-specific counters, that lie outside of the official C-language definition. Students will be expected to learn how to use the GNU Debugger ("gdb") program so that binary programs can be investigated.
Depending on the skills and interests of the students in this class, we may develop a BDD package. We may also investigate a SAT solver. For such analysis tools, I use the ACL2 system, and I may show several examples of using logic to verify hardware circuit or assembler program models. So, as time permits, we may learn the rudiments of Lisp -- one of the oldest programming languages.
In some cases, it may be helpful to reference documentation about the x86 architecture. We have placed some reference material in the documents directory. In some cases, students may be asked to read small sections from these documents. Note that these documents are large -- these documents are indicative of the complexity of the x86 architecture and, in general, of modern computer systems. Other companies than Intel (AMD and VIA) that develop and market x86 processors must fully comprehend the information contained in these documents. Unfortunately, the information contained in these documents is insufficient to develop a competitive x86 processor implementation. AMD offers their own manuals, which can be a place to look if the Intel documentation isn't sufficient. VIA doesn't publish any specification for their X86 implementations. Note, there are many undocumented features (e.g., caching read-ahead strategies, I/O ordering behavior, virtualization, context-switch mechanisms, encryption-and-decryption instructions, etc.) that are necessary to make an x86 processor perform well on a litany of common benchmarks. For an x86 processor to be competitive, it will need to contain these features. Although many x86 implementation mechanisms are protected by patents, anyone is now free to build their own 32-bit x86 implementation using Intel's IP as all of Intel's patents specific to the (32-bit x86) Pentium have expired.
For the adventurous student, special projects are possible. The content of a special project is pretty flexible -- so long as it has to do with specification and validation. For instance, I am interested in the development of an ISA model of IBM's Harvest computer, which was a extension of IBM's Stretch computer. Another possible specification project might involve some older microprocessor, e.g., the Motorola 68030 or the National Semiconductor NS32032. Or, a student might wish to formally specify RISC-V. Another project I'm looking for help with concerns booting FreeBSD or Linux on our evolving ACL2-based x86 ISA emulator. Other independent study projects are possible; please discuss your ideas with the instructor.
The value you get from this class will be directly related to the effort you (as a student) put forward. This class will require that you learn to work on your own, and this class may be less structured than many of the classes you have taken. For instance, I have taught CS429 many times, and when serving as an instructor for CS429, I lectured for many hours. In this class, there will be some lectures, but not nearly as many nor as long as is typical in CS429. The remainder of class time will be used to directly address problems and seek their solutions. If you have a laptop computer, you should bring it to class. In class, we will be doing some programming and discussing various issues, such as how the debugger or version control system functions. Eventually, all programming assignment must work on the CS Department Linux machines, but being able to use your own environment may speed your work and you may end up with more tools than when this class started. Having a laptop is not a requirement, but it will be very helpful for students to be able to individually access information during class, and when we are discussing programming issues it may be helpful for you to try things immediately. Note, it is possible to checkout a Linux-based laptop from the UTCS Department; check with the instructor if you wish to borrow such a laptop.
Students will be encouraged to give short (five- to ten-minutes) presentations in class on particular topics. When well done, these presentations can serve in place of a missed quiz or homework. In fact, any student may be called upon to give a two- or three-minute presentation on something being discussed in class or on their solution to a homework problem. Please come to class prepared to work; we will sometimes stop for a few minutes to make sure that everyone that has a chance to consolidate their thinking and to help students overcome problems with their understanding or with questions about the in-class presentations.
Our office hours are listed on the main class web-page. In addition, if you need help, you may certainly seek out and visit with the class TA and/or the instructor(s). You may arrange to meet us at other times than those listed, but you will need to send E-mail to arrange a time. If we become too busy during the scheduled office hours, we will expand our office hours to meet the needs of the students. If you cannot come to the scheduled office hours due to conflicts with other classes, let us know quickly so we can make arrangements to meet your needs.
The following gives an outline of what we will discuss. We are open to discussing other architecture topics of general interest, and we will include some of our own microprocessor design experience. The syllabus below is approximate; the exact rate at which we will cover some material will vary. Additional summary information about the class laboratories is available on the class laboratory and homework page.
Schedule Below is Approximate, Lectures Dates May Change Slightly
*** NOTE: Exam dates are tentative until January 31, 2019 ***
*** NOTE: Lab assignments and due dates are tentative until assigned ***
Class Date Short Description
00 Jan 23 Course Introduction
Sidebar: Getting your computing environment organized
01 Jan 28 C and Assembler programming,
Laboratory 0 assigned
02 Jan 30 C language interface, signature of main
03 Feb 4 C-language type signatures,
Binary Execution, Calling Convention
04 Feb 6 Binary File Layout, Core Images
Sidebar: Executable & library formats and
tools (ar, od, strings)
05 Feb 11 Computer Arithmetic Operations, Flags,
Laboratory 0 due, Laboratory 1 assigned
06 Feb 13 Discussion of Invariants, Practium
07 Feb 18 Invariant discussion, continued
08 Feb 20 Continue introduction to the use of invariant
09 Feb 25 Review of x86 architecture.
10 Feb 27 Introduction to "gdb", "od", "objdump".
In-class Pracitcum. Bring your laptops.
13 Mar 4 Programming with invariants. Exam Review
14 * Mar 6 In-class Exam
15 Mar 11 Exhibit formal verification techniques
Laboratory 1 due, Laboratory 2 assigned
16 Mar 13 Discussion of BDDs and BDD operations
Mar 18 -- 23 Spring Break
17 Mar 25 Computer Arithmetic Verification
18 Mar 27 Computer Arithmetic Verification Practium
19 Apr 1 Comparison Predicates
20 Apr 3 Comparison Predicates Practium
21 Apr 8 Back to Lab 2
22 Apr 10 Review Computer Arithmetic
23 Apr 15 Instruction Specification
24 Apr 17 Instruction Specification Practium
Laboratory 2 due, Laboratory 3 assigned
25 Apr 22 General Verification
26 Apr 23 ACL2-based verification
27 Apr 29 Selected student presentations,
28 * May 1 In-class Exam
29 May 6 In-class quiz worth two quiz grades,
Laboratory 3 due
30 May 8 In-class quiz worth two quiz grades,
Course Summary, Stump the Professor
There will be ten or so homework assignments given during the semester. On most weeks, homework will be assigned on Mondays and due nine days later (on Wednesdays) by class time. No homework will be assigned the last week of class, but there may be a homework due the last week of class. The two lowest homework grades will be dropped in the computation of the final homework grade. Homework will not be accepted late.
There will be two, in-class (70- to 80-minute) examinations. The material on exams will be cumulative. See the above schedule (marked with a * above) for the dates. There will be no final exam. There will be a number (five to eight) of unannounced "pop quizzes", and a quiz (worth double) on the last class. The lowest quiz grade will be dropped. Examinations must be taken at the scheduled times. Quizzes are offered at random times; each quiz will take 10 to 15 minutes.
There will be four (0, 1, 2, and 3) Laboratory Projects assigned. See the above schedule for dates. Once a laboratory due date has arrived, material addressed in that laboratory may appear on an exam. Laboratory assignments are important; performing the work necessary to complete the laboratories is the means by which you will solidify your understanding of the class material and the work that it takes to be a better programmer. Laboratory Projects may be turned in one week late, but no later than the last day of class. Late project submissions suffer a 20% reduction of the grade given for the content of the project.
For each laboratory, a lab report will be part of the requirement. As this course carries a writing flag, the quality and completeness of lab reports will count for 25% to 35% of the grade for the laboratory. So, it is important that you allot time and make a serious effort to provide the documentation required for each laboratory.
The weighting of the grades for the various aspects of the course are:
Component Percentage of Course Grade
Exam 1: 15%
Exam 2: 15%
Quizzes: 10%
Homework: 20%
Labs: 40% (see individual weighting just below)
The Laboratory Projects will be weighted as follows:
Laboratory Percentage of Course Grade
Lab 0: 5%
Lab 1: 10%
Lab 2: 15%
Lab 3: 10%
The grading for the entire course will be as follows:
Course Score Grade
[90 -- 100) A
[87 -- 90) A-
[85 -- 87) B+
[80 -- 85) B
[77 -- 80) B-
[75 -- 77) C+
[70 -- 75) C
[67 -- 70) C-
[65 -- 67) D+
[60 -- 65) D
[ 0 -- 60] F
Note the interval marks around the course-score column. For example,
a course grade of B will be assigned if your semester grade is greater
than or equal to 80 and less than 85. This also means that a course
grade of at least 67 needs to be achieved for this course to count
toward a UTCS degree.
The students who do well in this class are survivors. This class is a lot of work, and it is important to keep current. The material in this class is cumulative; it can be quite difficult to catch up if one falls behind. It is very important to keep turning in homework and laboratories. Generally, homework grades are our most reliable indicator of how well a student will do in this class. Note, it is important to show up for class, as pop quizzes are given, and material not reproduced in any particular book or web page may be discussed.
Return to CS340d course homepage.