|
|
Geoffrey Brown
Professor of Computer Science
Office address: Lindley Hall 330G,
Indiana University, Bloomington IN, 47405 USA
Office phone: 812-855-4207
Department fax: 812-855-4829
Email
Teaching
[C - H]335 Computer Structures
p436 Introduction to Operating Systems
C343 Data Structures and Algorithms
B639 Ensuring Long-term Access to Digital Information
b649 Concurrent Programming Languages for System Design
A major undertaking for the past several years has been the development
of a radically redesigned computer structures class (c335) which has as
its laboratory component a small robot built from a children's toy
Goofy Giggles.
The focus of this course is to build a bridge from a (relatively) high-level
language (C) to assembly code and its execution by a processor.
Course Spec
We are currently revising this course to use the ARM7 processor which is widely
used in embedded systems such as cell phones.
Research Interests
Digital system design methodology including formal verification,
software/hardware co-design, and reconfigurable computing. Digital
preservation.
I am exploring the use of off-the-shelf emulation and virtual
machine environments to support the digital archiving of documents
that require their original (obsolete) software for access. For example
the US Government Printing Office began distributing vital statistics
on CDROM with embedded proprietary software about 15 years ago - accessing
these data requires running the embedded software. To
see the current state of our online collection of GPO CDRoms -
http://www.cs.indiana.edu/svp/
We've
recently performed a study of 200,000 Office documents to determine
their resource requirements (fonts, helper applications, etc.) and
are undertaking a study with the Koninklijke Bibliotheek (Netherlands
National Library) to apply
our analysis tools to articles from their archive. The KB is the
digital repository for several major scientific publishers.
My work on cross-clock domain protocols has demonstrated that it
is possible to quickly verify real-time protocols using an off-the-shelf
model checker (SAL) that uses satisfiability-modulo-theories (SMT).
Previous efforts utilizing conventional theorem provers
required significant human (months vs days) and computer resources (hours
vs seconds) than
our approach.
Prior to my return to academia in 2003, I spent
seven years in industry where I co-led the HP side of the
Lx embedded VLIW microprocessor and its software system. This
was an HP Laboratories/ST
Microelectronics partnership and was the basis for the
the ST210, ST220, ST230, and ST231 processors. These
processors are embedded in many of ST's consumer electronics chips
often with multiple processor instances. For example,
there are three of these processors
in each STM8000 stm8000.pdf DVD recorder chip.
The Lx architecture is also used in digital video recorder chips
(stx5524,
stx5525, stm8010), set top box decoders
(sti5300,
sti5301), and in a new series
of HD H264 set top box chips as the st231
(stb7100,
sti7101,
sti7105,
sti7109,
sti7111,
sti7141,
stb7200).
I also worked as a software architect for
several networking startups, most recently as chief architect of Sockeye
Networks. At Sockeye Networks I developed a system for Internet
address clustering to support intelligent route optimization. This
system allowed Sockeye Networks to save millions of dollars by replacing
data purchased by other companies.
My verification work is a continuation of my long history of studying
design, verification, and synthesis techniques for digital systems.
I performed early and widely cited work on the
design of self-stabilizing systems which have the desirable property that,
when started in any state, are guaranteed to converge to a desirable state in
finite time. My work on the design and verification of multiprocessor cache
algorithms, in particular "Lazy Caching" was the subject of a special issue
of Distributed Computing. I've also developed techniques to verify hardware
synthesis algorithms.
Selected Publications
Digital Preservation
- K. Woods and G. Brown. "Creating Virtual CD-ROM Collections,"
International Journal of Digital Curation, 4(2), 2009.
http://www.ijdc.net/index.php/ijdc/article/view/128
- K. Woods and G. Brown. "Assisted Emulation for Legacy Executables",
5th International Digital Curation Conferences, 2009.
- K. Woods and G. Brown. "Born Broken: Fonts and Information Loss in
Legacy Digital Documents," Sixth International Conference on Preservation
of Digital Objects iPRES, 2009.
- K. Woods and G. Brown. "Migration Performance for Legacy
Data Access," International Journal of Digital Curation,
3(2), 2008. http://www.ijdc.net/index.php/ijdc/article/view/88
- T. Reichherzer and G. Brown. "Quantifying Software
Requirements for Supporting Archived Office Documents Using Emulation",
Joint Conference on Digital Libraries (JCDL), 2006.
http://doi.acm.org/10.1145/1141753.1141770.
- G. Brown. "Virtualizing the CIC Floppy Disk Project",
Fall Depository Library Conference, 2006.
http://www.access.gpo.gov/su_docs/fdlp/pubs/proceedings/06fall/brown.pdf
Draft paper http://www.cs.indiana.edu/ geobrown/jcdl.pdf
Verification of Cross Clock Domain Protocols
- G. Brown and L.Pike. "Automated Verification and Refinement for Physical-Layer
Protocols", To appear in Formal Aspects of Computing.
DOI:10.1007/s00165-010-0149-0.
- L. Pike, G. Brown and A. Goodloe. "Roll Your Own Test Bed For Embedded
Real-Time Protocols: A Haskell Experience", Haskell Symposium, 2009.
- G. Brown and L. Pike. "Temporal Refinement Using SMT and
Model Checking with an Application ot Physical-Layer Protocols",
Proceedings of Formal Methods and Models for Codesign (MEMOCODE), 2007.
- G. Brown. "Verification of a Data Synchronization Circuit For All Time",
6th International Conference on Application of Concurrency to System Design, (ACSD 2006).
- G. Brown and L. Pike. "Easy Parameterized Verification of Biphase Mark and 8N1 Decoders,"
International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, (TACAS 2006)
Lecture Notes in Computer Science 3920. pp. 58-72.
http://dx.doi.org/10.1007/11691372
- G. Brown and L. Pike. ""Easy" Parameterized Verification of Cross Clock-Domain Protocols,"
Designing Correct Circuits, April 2006.
Embedded System Software
- B. Pisupati, G. Brown. "File System Interfaces for Embedded Software
Development," IEEE International Conference
on Computer Design, October 2005, pp. 232-238.
pdf file
http://dx.doi.org/10.1109/ICCD.2005.57
- S. Tilak, B. Pisupati, K. Chiu, G. Brown, and N. Abu-Ghazaleh.
"A File System Abstraction for Sense and Respond Systems,"
EESR 05: Proceedings of the 2005
Workshop on End-to-End, Sense-and-Respond Systems, Applications,
and Services, June 2005, pp 1-6.
pdf file
VLIW Microprocessor
- P. Faraboschi, G. Brown, J. A. Fisher, G. Desoli, and F. Homewood.
"Lx: A Technology Platform for Customizable VLIW Embedded Processing,"
Proceedings of International Symposium of Computer Architecture, pp. 203-213,
June 2000.
pdf
file
http://doi.acm.org/10.1145/339647.339682
-
US 7,779,240. M. Homewood, G. Vondran, G. Brown, P. Faraboschi.
System and Method for Reducing Power Consumption in a Data Processor
Having a Clustered Architecture, 2010.
-
US 7,337,306. M. Homewood, G. Vondran, G. Brown, and P. Faraboschi.
Executing Conditional Branch Instructions in a Data Processor Having a
Clustered Architecture, 2008.
-
US 7,143,268. M. Homewood, A. Jarvis, G. Brown, P. Faraboschi, and G. Vondran.
Circuit and Method for Instruction Compression and Dispersal in
Wide-Issue Processors, 2006.
-
US 6,922,733.
M. Homewood, A. Jarvis, A. Starr, G. Brown, P. Faraboschi,
and Gary Vondran.
System and Method for Encoding Constant Operands in a Wide Issue
Processor, 2005.
pdf file
-
US 6,691,210. P. Faraboschi, A. Starr, G. Brown, and R. Ford
Circuit and Method for Hardware-Assisted Software Flushing of
Data and Instruction Caches, 2004.
pdf file
-
US 6,829,700. P. Faraboschi, A. Starr, G. Brown, and M. Homewood
Circuit and Method for Supporting Misaligned Accesses in the
Presence of Speculative Load Instructions, 2004.
pdf file
Internet Address Clustering
- G. Brown. "Internet Address Clustering for Intelligent Route
Control." (Unpublished)
pdf file
- G. Brown.
"Network Address Space Clustering Employing Topological Groupings, Distance Measuremetns, and Structural Generalization". US Patent application 20040059830.
pdf file
Self-Stabilization
- Y. Afek and G. M. Brown. "Self-Stabilization over Unreliable
Communication Media," Distributed Computing,7, pp. 27-34, 1993.
http://dx.doi.org/10.1007/BF02278853
- G. M. Brown, M. G. Gouda, and C-l. Wu. "Token Systems that
Self-stabilize," IEEE Transactions on Computers, vol. 38, no. 6, pp.
845-852, June 1989.
http://doi.ieeecomputersociety.org/10.1109/12.24293
Cache Consistency
- Y. Afek, G. M. Brown, and M. Merritt. "Lazy Caches," ACM
Transactions on Programming Languages and Systems, vol. 15, no. 1, pp.
182-205, January 1993.
pdf file
http://doi.acm.org/10.1145/151646.151651
This paper was the subject of a special double issue
of Distributed Computing, 12(2/3), 1999.
http://dx.doi.org/10.1007/s004460050056
- G. M. Brown "Asynchronous Multicaches," Distributed Computing,
vol. 4, no. 1, pp. 31-36, 1990.
http://dx.doi.org/10.1007/BF01783663
Hardware Synthesis
- J. O'Leary, G. M. Brown, and W. Luk. "Verified Compilation of
Communicating Processes into Clocked Circuits," Formal Aspects of
Computing, vol. 9, pp. 537-559, 1997.
pdf file
http://dx.doi.org/10.1007/BF01211459
- G. M. Brown, W. Luk, and J. O'Leary. "Retargeting a Hardware Compiler
Using Protocol Converters." Formal Aspects of Computing, vol. 8, pp.
209-237, 1996.
http://dx.doi.org/10.1007/BF01211459
- J. He, G. M. Brown, W. Luk and J. O'Leary. "Deriving Two-phase Modules
for a Multi-Target Hardware Compiler," in Designing Correct Circuits,
Springer Electronic Workshop in Computing Series, 1996.
pdf file
Other
Using the STM32VLDISCOVERY board http://cgi.cs.indiana.edu/ geobrown/stm32
File translated from
TEX
by
TTH,
version 3.61.
On 10 Jan 2011, 17:33.
|
