Automatic Client-Server Partitioning

The automatic client-server partitioning is a technique to partition an application functionality across the client-server boundary automatically.

Some of systems supporting the automatic client-server partitioning include:

• Hilda
• Links
• Swift

OKL4 (or seL4) Released.

On January 21st, 2011, there was an announcement that Open Kernel Labs released OKL4 Verified for download and prototyping.

http://www.ok-labs.com/releases/release/open-kernel-labs-provides-okl4-verified-for-download-and-prototyping

• OK-labs Developer Wiki : http://wiki.ok-labs.com/
• OK GeekTV http://www.ok-labs.com/community/ok-geektv/
• White papers http://www.ok-labs.com/products/whitepapers-abstract-page
• Blogs http://www.ok-labs.com/community/company-blog
• Book in Amazon : (Open Kernel Labs)

1. What are released

The seL4 ARM binaries both on ARM and IA32 are released. For each architecture, two binaries are available: one for debug mode and the other for release mode.

It provides the source codes for user libraries to make use of the released binary kernels. One can build several examples to pack it with the seL4 kernel to run on a version of Qemu supporting ARM architecture. For this, it provides an Elf loader (ARM boot loader) and a binary file manipulator (Dite).

A para-virtualised Linux, Wombat, is also included as an example. But it can run either on a Qemu supporting IA32 or a real hardware.

Open Kernel Labs released the seL4 Reference manual for API version 1.1 together with an abstract formal specification for the APIs. The specification is written in Isabelle/HOL definitions.

1.1 What are not released

Note that the source code for the seL4 kernel is not opened. As a natural consequence, it provides no concrete formal specification and no proof things. It is unfortunate not to be able to see a high-level prototype, written in Haskell, of the seL4 kernel that matches with the released abstract specification.

2. Playing with the seL4 examples

It seems to be quite straightforward to run the released seL4 examples. I ran them on Ubuntu 10.04. You have only to follow the instructions guided by . 

Some of the released examples run on ARM while the others run on IA32. You had better download two set of Code Sourcery toolchains. (Can we build the IA32 examples with the gcc compiler on the Ubuntu?)

This is just for your reference, I downloaded two Sourcery G++ Lite 2010.09-50 for ARM GNU/Linux and 2010.09-44 for IA32 GNU/Linux to build the released examples.

My quick trials succeeded in building and running the examples in Section 1,2,3,4, but got stuck in Section 5 and 6. (I will continue to explore the reason of the build errors I met.)

3.

(Soon I will try to write a summary of the API reference and the abstract specification.)

Quantifier Elimination

Quantifier elimination is a method of transforming a formula into an equivalent quantifier-free formula. Since quantifier-free formulae are easy to reason, quantifier elimination is useful for deduction and many quantifier-elimination procedures have been developed. Above all, quantifier-eliminationprocedures called "quantifier elimination by virtual substitutions" are known to be suitable for practical implementation. The idea of the virtual substitution based methods is to use a finit set of test cases, called an elimination set.

• B. F. Caviness, and J.R. Johnson (eds.), Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer, Heidelberg, 1998.
• R. Loos and V. Weispfenning, Applying Linear Quantifier Elimination, Computer Journal, Vol.36, No. 5, pp450-462, 1993.
• How to obtain elimination sets
• A. Dolzmann and T. Sturm, Simplification of Quantifier-Free Formulae over Ordered Fields, Journal of Symbolic Computation, Vol. 24, No. 2, pp209-231, 1997. 
• How to simplify quantifier-free formulae

Emscripten: an LLVM-to-JavaScript compiler

It is very stunning to find Emscripten, a compiler of LLVM bitcodes into JavaScript. The LLVM bitcodes can be generated from C/C++ using llvm-gcc or clang or any other languages that can be converted into LLVM. The generated JavaScript can run on the WEB!

http://code.google.com/p/emscripten/

Near Field Communication (NFC)

What is NFC


Simply speaking, it is a technology that combines the funtion as a RFID tag and the function as a RFID reader! NFC defines three communication modes: peer-to-peer mode, read/write mode, and NFC card emulation mode. 

• http://www.nfc-forum.org/home/
• http://www.stolpan.com
• http://en.wikipedia.org/wiki/Near_Field_Communicati
• http://www.itdaily.kr/news/articleView.html?idxno=18297 (In Korean)

Standards

• ISO/IEC 14443 : Identification cards, Contactless integrated circuit cards, Proximity cards
• ISO/IEC 18092 : NFCIP-1 (NFC Interface Protocols) http://www.nfc-world.com/en/about/ 참고
• JIS X 6319-4 : FeliCa
• ISO/IEC 15693 : Vicinity cards

Research Institute

• http://www.nfc-research.at
• http://mocs.vtt.fi/

NFC Implementations


Android NFC API supports Read NDEF messages, and SUN JSR-257 supports read/write mode and NFC card emulation mode. NFCIP and Libnfc support peer-to-peer mode in Java and in C, respectively.

• Open NFC Software Stack : http://www.open-nfc.org sponsored by InsideSecure
• Hardware neutral due to NFC HAL
• Available  for Android, PC, WinCE, Linux, Java Applets, and Java Apps
• Android 2.3 : http://developer.android.com/resources/samples/NFCDemo/
• The Android NFC API in Gingerbread supports an adapter to NFC device and a NDEF(NFC Data Exchange Format) message library.
• SUN, The Contact less Communication API, JSR-257 http://java.sun.com/developer/technicalArticles/javame/nfc/
• NFCIP (Peer 2 Peer) in Java SE and MIDP : http://code.google.com/p/nfcip-java/
• Libnfc in C : http://www.libnfc.org/
• Stollmann http://www.stollmann.de/en/stacks/nfc.html
• Trusted Logic : http://www.trusted-logic.com/spip.php?rubrique27
• Open Source Library to enable P2P over NFC (available for Android) :  http://code.google.com/p/ismb-npp-java/

 Workshop

• RFID Security : http://www.rfid-sec.org/
• Global NFC Congress : http://www.wima.mc/
• NFC Forum Spotlight for Developers :  http://www.nfc-forum.org/events/oulu_spotlight/
• Global NFC Applications Products & Services Congress : http://www.wima.mc/

News on 2011's NFC

• Near Field Communication World : http://www.nearfieldcommunicationsworld.com/
• http://stonefocus.thoth.kr/?mid=blog&document_srl=7563920 (In Korean)
• http://www.zdnet.co.kr/Contents/2010/10/13/zdnet20101013100228.htm (In Korean)

Products

• NXP Mifare http://mifare.net
• Samsung Nexus S used the NXP PN544 chip.

NFC Applications

• MyNFC, an open source, Java Script based development environment
• It looks like web widgets supporting NFC interfaces. But not sure how NFC tags are integrated into the Java Script environment. 
• http://daw.mynfc.org/mynfc.org
• http://sourceforge.net/projects/mynfc/develop