Soonho Kong

Synergy, Security, and Tips

This article introduces how to set up synergy, a tool which lets you easily share your mouse and keyboard for multiple computers.

Introduction

More displays mean better productivity to me. Currently, I’m using five – two for emacs, one for terminal, one for email, one for web search – and I find them very useful.

Ideally, you may have a computer and a special hardware such as KVM switches or Matrox TripleHead2Go which connects multiple monitors to a single machine. However, they are pretty expensive and not an option for a poor graduate student like me.

The alternative is to have multiple machines, each connected to one or two displays. Then, you can use synergy to control them with a single mouse/keyboard. In my case, I have two desktops and one laptop. With shared clipboard feature, you have an illusion of having a single machine with multiple displays.

Basic Setup

In this article, I explain the set up based on my configuration. I have Macbook Air, iMac, and a Linux machine. We will install synergy server on the Linux machine and two clients on Macbook Air and iMac.

Linux (server)

  • Download and install synergy from the webpage.
  • I’m using version 1.4.12, protocol version 1.4
  • Save the following file as ~/.synergy.conf. You may need to edit screens and links section. You also need to provide an IP address of each machine in aliases section.
# +--------+ +--------+ +-------+
# | Mac Air| | Linux  | | iMac  |
# +--------+ +--------+ +-------+

section: screens
Linux:
halfDuplexCapsLock = false
halfDuplexNumLock = false
halfDuplexScrollLock = false
xtestIsXineramaUnaware = false
switchCorners = none
switchCornerSize = 0

iMac:
halfDuplexCapsLock = false
halfDuplexNumLock = false
halfDuplexScrollLock = false
xtestIsXineramaUnaware = false
switchCorners = none
switchCornerSize = 0

MacAir:
halfDuplexCapsLock = false
halfDuplexNumLock = false
halfDuplexScrollLock = false
xtestIsXineramaUnaware = false
switchCorners = none
switchCornerSize = 0
end

section: links
Linux:
right = iMac
left = MacAir
iMac:
left = Linux
MacAir:
right = Linux
end

section: options
relativeMouseMoves = false
screenSaverSync = true
win32KeepForeground = false
switchCorners = none
switchCornerSize = 0
end

section: aliases
Linux:
<IP of Linux>
iMac:
<IP of iMac>
MacAir:
<IP of MacAir>
end
  • You can start synergy daemon by typing
synergys --daemon --name Linux -c ~/.synergy.conf

Mac (client)

I found problems using the client that I get from http://synergy-foss.org. It seems Quicksynergy works on my Mac machines. You can start the client by typing

/Applications/QuickSynergy.app/Contents/Resources/synergyc \
                            --name <CLIENT_NAME> localhost

In my configuration, <CLIENT_NAME> is either iMac or MacAir.

Security Issue

The above setup has a security issue. Whatever you type will be sent from the server (Linux) to the other machines (iMac/MacAir) as a plain text. It means that any computer in the same network can see what you type including passwords. This could be problem if you are on a school/company network.

Synergy recently started to provide encryption methods. However, there is a recent article discussing the problem of the current encryption methods and possible attacks on them.

However, we can still rely on SSH tunneling. Simply put, we create a secure channel of communication between a server and clients. Then, let synergy use the channel to exchange information.

In server (linux), we start synergy daemon with --address :24800 option to specify the port number which we use as a tunnel.

/usr/bin/synergys --daemon --name Linux -c ~/.synergy.conf --address :24800

In client, we first establish the SSH tunnel and run synergy client:

ssh -f -N -L localhost:24800:<SERVER-HOSTNAME>:24800 <SERVER-HOSTNAME>
/Applications/QuickSynergy.app/Contents/Resources/synergyc \
                                        --name <CLIENT_NAME> localhost

Here <SERVER-HOSTNAME> is either IP address or domain name of the server.

Tip: Keyboard Shortcut to Navigate Screens

Having multiple monitors create a new problem. It takes some time to move the mouse pointer from one side to the other side (in my case, it’s about 5400px to cross). Fortunately, synergy provides a solution for this problem. You can add the following to the ~/.synergy.conf file on the server.

section: options
keystroke(shift+alt+left) = switchInDirection(left)
keystroke(shift+alt+right) = switchInDirection(right)
end

Now you can press shift+alt+left/right to move the focus to the left and right.

Tip: Wakeup Script

There is a possible problem when the computers go to the sleep mode. You can wake up the computer which has a mouse and keyboard connected. However, there are no ways to wake up the other machines. In my case, they are Mac machines and I found the following “wakeup” script from the web.

#include <CoreFoundation/CoreFoundation.h>
#include <IOKit/IOKitLib.h>

#include <iostream>

void set_request_idle(bool request)
{
    io_registry_entry_t entry = IORegistryEntryFromPath(kIOMasterPortDefault,
            "IOService:/IOResources/IODisplayWrangler");
    if (entry == MACH_PORT_NULL) {
        return;
    }

    IORegistryEntrySetCFProperty(entry, CFSTR("IORequestIdle"),
            request ? kCFBooleanTrue : kCFBooleanFalse);

    IOObjectRelease(entry);
}

int main(int argc, const char **argv)
{
    const std::string &command = (argc > 1) ? argv[1] : "";

    if (command == "idle") {
        set_request_idle(true);
    } else if (command == "wake") {
        set_request_idle(false);
    } else {
        std::cerr << "usage: " << argv[0] << " (idle|wake)\n";
        return 1;
    }

    return 0;
}

You can save the file as wakeup.cc and compile it on Mac as follows.

clang++ -Wall -O3 -framework Foundation -framework IOKit wakeup.cc \
        -o ~/bin/wakeup

Then you can ssh from the server to a client and remotely execute the wakeup script as follows:

(SERVER) $ ssh <CLIENT_IP> "~/bin/wakeup wake"

How to Install and Migrate CDash Server

This article introduces how to install and migrate CDash server. In Lean and dReal projects, we are using CDash as a data sink, where we store build logs, test results, code coverages, and dynamic analysis results of projects.

Install CDash

Required Packages

In Ubuntu 12.04.03 LTS, we need to first install the following packages:

sudo apt-get install apache2 php5 php5-xsl php5-curl php5-gd \
                     mysql-server-5.5 mysql-client-5.5 php5-mysql

During the installation, you will be asked to create a mysql-root password.

Check out CDash

cd /var/www
svn co https://www.kitware.com/svn/CDash/Release-2-0-2 CDash

Setup MySQL User and Database

We create a MySQL user cdash and a database cdash and set up permissions.

$ mysql -u root -p
<HERE YOU TYPE YOUR MYSQL ROOT PASSWORD>

mysql> create database cdash;
mysql> create user 'cdash'@'localhost' identified by '<YOUR_PASSWORD_GOES_HERE>';
mysql> grant all privileges on cdash.* to 'cdash'@'localhost' with grant option;

Configure CDash

It is recommended to create a local copy of CDash/cdash/config.php.

cd CDash/cdash
cp config.php config.local.php

Then, we need to modify config.local.php.

// Hostname of the database server
$CDASH_DB_HOST = 'localhost';
// Login for database access
$CDASH_DB_LOGIN = 'cdash';
// Port for the database (leave empty to use default)
$CDASH_DB_PORT = '';
// Password for database access
$CDASH_DB_PASS = '<MySQL CDASH PASSWORD GOES HERE>;
// Name of the database
$CDASH_DB_NAME = 'cdash';
// Database type (empty means mysql)
$CDASH_DB_TYPE = 'mysql';

Directory Permission

www-data needs to own backup, upload, and rss directory.

cd /var/www/CDash
sudo chown www-data backup upload rss

Install CDash via WWW

Using a web-browser, open http://<YOUR_SERVER>/CDash/install.php. You will be asked to put admin email and admin password.

Enable Production Mode

Once, CDash is installed correctly, change cdash/config.local.php file to enable production mode.

...
$CDASH_PRODUCTION_MODE = true;
...

Migrate CDash Server

Let’s consider a scenario in which we move CDash data from server A to server B.

In Server A

Dump cdash database using mysqldump

mysqldump -u cdash -p cdash > backup.sql

In Server B

Reconstruct cdash database from backup.sql

mysql -u cdash -p cdash < backup.sql

git pre-push hook

This article introduces git pre-push hook.

Problem

In Lean project, we use a modified version of Google’s C++ style checker. I want to automatically run the checker over the changed files before I push commits to git repositories. This is useful because it prevents me from accidentally pushing the commits which contain style problems.

Solution: git pre-push hook

Since git 1.8.2, git introduced pre-push hook which is executed before actual push operation is performed. The following two steps solve the problem.

  • Create <PROJECT_ROOT>/.git/hooks/pre-push file with the following contents:
#!/usr/bin/env bash
IFS=' '
DIR="$( cd "$( dirname "$0" )" && pwd )"
CHECKER=$DIR/../../src/cmake/Modules/cpplint.py
while read local_ref local_sha remote_ref remote_sha;
do
    CHANGED_FILES=`git diff --name-only $local_sha $remote_sha | grep '\(cpp\|h\)$'`
    if [ ! -z "$CHANGED_FILES" -a "$CHANGED_FILES" != " " ]; then
        echo $CHANGED_FILES | xargs $CHECKER
        RET=$?
        if [ $RET -ne 0 ]; then
            echo "There is error(s) from style-check. Please fix them before push to the repo."
            exit $RET
        fi
    fi
done
exit 0
  • Give “exec” permission to the file
chmod +x <PROJECT_ROOT>/.git/hooks/pre-push

Note that you need to change CHECKER variable if you want to use other checkers.

MXE: cross-compile windows binaries on ubuntu

This article introduces MXE (M cross environment) which helps set up a cross-compilation environment on *nix systems. Here, I use Lean theorem prover as a target program to illustrate the process.

Problem

I wanted to build a windows binary of Lean theorem prover while satisfying the following constraints:

  1. need C++11-compatible compilers: gcc (>=4.8) or clang (>= 3.3)
  2. need additional libraries – gmp, mpfr
  3. want to avoid CYGWIN, you know w-h-y
  4. prefer to build (cross-compile) on Linux/OS X to integrate with our automatic build system

Solution: MXE

I found that MXE can satisfy all the constraints:

MXE (M cross environment) is a Makefile that compiles a cross compiler and cross compiles many free libraries…

  • It uses mingw-w64.
  • You can easily compile gcc and other libraries such as gmp and mpfr.
  • It supports cmake, which makes my life easier.

Setup

  • Check out MXE:
cd /tmp/
git clone -b stable https://github.com/mxe/mxe.git
  • Build gcc, gmp, mpfr, winpthreads and lua. MXE_TARGETS=x86_64-w64-mingw32 specifies that we only build for the x86_64 architecture. -j4 means upto four packages are built in parallel (inter-package) and JOBS=4 allows four compiler processes to compile a package in parallel (intra-package).
make MXE_TARGETS='x86_64-w64-mingw32' gcc gmp mpfr winpthreads lua -j4 JOBS=4
  • By default, gcc is configured with --enable-threads=win32 and it does not support C++11 <thread>, <mutex>, or <future> (for more information, read this). To support C++11, we need to configure gcc using posix threads. Modify the line 12 and 43 of src/gcc.mk:
...
 12: $(PKG)_DEPS     := binutils gcc-cloog gcc-gmp gcc-isl gcc-mpc \
                        gcc-mpfr winpthreads
...
 43:         --enable-threads=posix \
  • Make gcc again. Yes, you need to build gcc twice due to the circular dependency between winpthreads and gcc. (Please let me know if you know a better way)
make MXE_TARGETS='x86_64-w64-mingw32' winpthreads gcc -j4 JOBS=4

Cross-compile Lean with cmake

After setting up mxe, type the followings to cross-compile Lean:

cd <LEAN_DIR>
mkdir build/release-cross
cd build/release-cross
cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src -DTCMALLOC=OFF \
 -DCMAKE_TOOLCHAIN_FILE=/tmp/mxe/usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake
make

Precompiled Environment

I prepared a cross-compilation environment which can be used to compile Lean in Ubuntu systems. To use it, please follow the instructions:

cd /tmp
mkdir mxe
cd mxe
wget http://dl.dropboxusercontent.com/u/203889738/gcc/mxe-gcc-4.8.2.tar.bz2
tar xvfj mxe-gcc-4.8.2.tar.bz2

How to use newer version of GCC

We found a problem while using the default gcc shipped with MXE – gcc-4.8.2. When thread_local is used in a program, gcc-4.8.2 generates a binary which crashes when executed.

To fix this, we use the latest version of gcc-4.8, gcc-4.8.3 (snapshot 20131205). To use this, you need to modify the top part of src/gcc.mk as follows:

# This file is part of MXE.
# See index.html for further information.

PKG             := gcc
$(PKG)_IGNORE   :=
$(PKG)_VERSION  := 4.8-20131205
$(PKG)_CHECKSUM := b5e77ad4395561ac3f13f3a635ed5d704bab3786
$(PKG)_SUBDIR   := gcc-$($(PKG)_VERSION)
$(PKG)_FILE     := gcc-$($(PKG)_VERSION).tar.bz2
$(PKG)_URL      := ftp://ftp.mirrorservice.org/sites/sourceware.org/pub/gcc/snapshots/4.8-20131205/$($(PKG)_FILE)
$(PKG)_DEPS     := mingwrt w32api mingw-w64 binutils gcc-gmp gcc-mpc gcc-mpfr

Basically, you can follow the same instructions to build a cross-compile environment using gcc-4.8.3 (20131205). We also prepared a pre-compiled one using gcc-4.8.3. You can download it at here.

Known Issue

cmake-2.8.12 has a conflict with usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake. In mxe-conf.cmake, it resets CMAKE_FIND_ROOT_PATH and it affects CMAKE_DETERMINE_COMPILER_ID function which is modified in version 2.8.12. For now, it is best to use version 2.8.11.2.

Projectile and Ack-and-a-half Emacs modes

I introduce two emacs modes – projectile and ack-and-a-half – which I found very useful to solve common tasks that I have in programming.

Problem

I want to have an efficient way to do the following tasks:

  • open a file in a project
  • run grep on the files in a project

Certainly, ido-mode and find-grep help achieve the goals, but they do not understand the project boundary and require extra works as a result.

For instance, consider a scenario that you are editing src/kernel/expr.h. To open src/tests/kernel/expr.cpp, you need to move up to src/ and go down to src/tests/kernel/expr.cpp. To find all the files containing “expr” in the project, you may run find-grep. However, you need to manually specify the project root directory in which find starts its search.

Projectile

projectile is a solution for the problem. It automatically detects the project root using version control information such as git and helps us perform project-level operations with a few key strokes. Here are some of its features:

  • C-c C-p f: Display a list of all files in the project
  • C-c C-p d: Display a list of all directories in the project
  • C-c C-p a: Runs ack (something like grep) on the project
  • C-c C-p c: Runs a standard compilation command

Installation is easy via package-install command in Emacs 24.3. You need to install projectile and ack-and-a-half (for ack that I will explain in the next section). Here is the emacs-lisp setting file that I’m using (note that I redefine the prefix as C-c C-p):

(setq projectile-indexing-method 'git)
(setq projectile-enable-caching t)
(setq projectile-keymap-prefix (kbd "C-c C-p"))
(projectile-global-mode t)
(let ((ack_path "~/bin/ack"))
  (if (file-exists-p ack_path)
      (setq ack-and-a-half-executable ack_path)
    )
  )

Ack: Beyond grep

ack is a tool like grep, optimized for programmers. It claims to have many advantages over grep. With projectile and ack-and-a-half emacs-mode, you can search a string over all files in a project wherever you are. Ack-and-a-half create a compilation buffer in which you can navigate the result efficiently.

To install ack, please type the following in the terminal.

curl http://beyondgrep.com/ack-2.10-single-file > ~/bin/ack && chmod 0755 !#:3

You can also create .projectile at the project root, to specify a set of files and directories that you want to exclude from its operations. For instance, I have the following for Lean project to exclude build directory from the search.

-/build

Running (Secure) Wordpress @ CMU

By default, CMU web servers do not allow you to run scripts written in PHP, Ruby, Perl, and Python. However there is a way to enable this feature by using http://www.contrib.andrew.cmu.edu web server.

First step

Read whoji’s post on How to setup wordpress on Andrew File System(AFS) @ CMU. Though it’s not complete, it’s very good point to start. He explains every step in detail so that it should be quiet easy to follow. Once you followed his instructions, you have a working wordpress blog on your account. Here, I assume that you installed the blog at ~/www/blog.

Problem: Security Issue

So, what’s the problem? Even if your-just-installed-blog works now, there is a security problem in this configuration. Because of the way AFS works, any user in the AFS system can access your wp-config.php file where you put your MySQL user ID and password!

Please note that changing linux permission on your blog directory does not help. If you read Computer Club’s documentation, you will find that they already mentioned this problem (and also a possible solution).

Solution

Script are run by contrib.your_andrew_ID@club.cc.cmu.edu account. Therefore, the solution is to put wp-config.php file into a directory where no one but contrib.your_andrew_ID has an access and use that file instead of the one at ~/www/blog. Here, we use ~/www/blog/secret as an example.

  1. Create a folder where you hide your wp-config.php file.

    ~/www/blog> mkdir secret
    
  2. Move wp-config.php to the secret directory

    ~/www/blog> mv wp-config.php secret/
    
  3. On the secret folder, give no permission to system:anyuser:

    ~/www/blog/secret> fs sa . system:anyuser none
    
  4. Give read/listing permissions to contrib.your_andrew_ID@club.cc.cmu.edu:

    ~/www/blog/secret> fs sa . contrib.your_andrew_ID@club.cc.cmu.edu rl
    
  5. Substitute all the occurrences of wp-config.php with secret/wp-config.php in ~/www/blog/wp-load.php and ~/www/blog/wp-admin/setup-config.php files.

LaTeX Template for Statement of Purpose

The SOP (Statement of Purpose) season is back! and I got requests from my friends to review and help them polish up their SOPs. I wanted to share my LaTeX template for SOP with them. Please feel free to use it.

Requirement

  • It uses Adobe Caslon Pro font family. If you don’t have them, you cannot compile the SOP. For more information about the fonts, please visit here.

How to Compile

It uses xelatex to use custom fonts. After modifying the downloaded main.tex, type the following on the terminal:

$ xelatex main.tex

I only tested it on OSX machines, you may have problems on other platforms such as Windows or Linux.

Programming Turing Machines

In the previous post, we built a LEGO Turing machine. However, we did not talk about how to run the machine. In this post, we focus on how to program Turing machines. Starting from a very naive implementation which only uses a single task, we will add more features to the machine incrementally:

  • multi-task
  • concurrent movements
  • log via USB
  • support its own programming language
  • transfer a program via USB

Turing Machine

Turing Machine is an abstract computing device which was contrived by Alan Turing. It runs the following algorithm:

  1. Read : Read the current cell of the tape.
  2. Transition : Determine the next state, output, and shift direction based on the current state and the content of the current cell. If the new state is either Accept or Reject state, stop the machine.
  3. Write : If needed, change the value of the current tape cell.
  4. Move : Move the tape to the left or right based on the result of 2.
  5. Goto 1.

1. Simple, Single-task Turing Machine (Download)

We start with a simple implementation. This implementation has the following properites (limitations):

  • Single-task
  • Controlled by a Transition Relation
  • Serialized Movement: Read - Write - Move, one by one.
  • No Logging

1.1 Main Loop

Main code of the simple Turing Machine
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
TASK(TM)
{
    while(true)
    {
        /* Read */
        input = Read();

        /* Make transition */
        (state, output, dir) = transition(state, input);
        if(state == HALT_STATE)
            HALT;

        /* Write (Optional) */
        if(input != output) {
            write(output);
        }

        /* Move */
        move(dir);
    }
}

The main loop is a direct translation of the algorithm presented above. Repeatedly, it reads the tape cell, makes a transition which is defined in transition function, optionally changes the current tape cell, and moves the tape as directed.

1.2 Reader

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
_Bool read()
{
    U16 color;
    _Bool input;

    /* 1. Move READ Header to TAPE */
    nxt_motor_set_speed(READ_MOTOR, SPEED, 1);
    while(nxt_motor_get_count(READ_MOTOR) <= READ_REV) {
        /* do nothing */
    }
    nxt_motor_set_speed(READ_MOTOR, 0, 1);

    /* 2. Read Sensor Value */
    ecrobot_set_nxtcolorsensor(COLOR_SENSOR, NXT_LIGHTSENSOR_GREEN);
    ecrobot_process_bg_nxtcolorsensor();
    color = ecrobot_get_nxtcolorsensor_light(COLOR_SENSOR);
    input = color < COLOR_THRESHOLD ? 1 : 0;
    ecrobot_set_nxtcolorsensor(COLOR_SENSOR, NXT_LIGHTSENSOR_NONE);
    ecrobot_process_bg_nxtcolorsensor();

    /* 3. Move READ Header back */
    nxt_motor_set_speed(READ_MOTOR, -SPEED, 1);
    while(nxt_motor_get_count(READ_MOTOR) >= 0) {
        /* do nothing */
    }
    nxt_motor_set_speed(READ_MOTOR, 0, 1);

    return input;
}

read function does three operations:

  1. Move the READ header to the TAPE
  2. Read the sensor value
  3. Move the READ header back

Let’s focus on the actual reading operation (in step 2) because it is relatively trivial to move the header back and forth (step 1 & 3). At line 14, it turns on the color sensor and set it to NXT_LIGHTSENSOR_GREEN mode. At line 16, ecrobot_get_nxtcolorsensor_light function returns the raw value which measures the reflection around the sensor. We use the pre-defined constant COLOR_THRESHOLD to determine whether the given raw value is interpreted as 0 or 1. (line 17). Then, it turns off the light sensor (line 18).

Note that it is necessary to call ecrobot_process_bg_nxtcolorsensor function at line 15 and line 19. When we change the sensor mode by calling ecrobot_set_nxtcolorsensor at line 14, nothing really happens on the sensor side. It only changes the sensor status on the memory without affecting the sensor itself. It is the job of ecrobot_process_bg_nxtcolorsensor function which makes requested changes on the sensor side and copies the raw value of the sensor to the memory. If we do not call ecrobot_process_bg_nxtcolorsensor at line 14, 1) the sensor is not set to green light mode and 2) the value we read at line 16 can be an outdated value– it is the value of the sensor when ecrobot_process_bg_nxtcolorsensor function was called last time.

1.3 Writer

1
2
3
4
5
6
7
8
9
10
11
void write(_Bool output)
{
    int sign = output == 1 ? 1 : -1;
    nxt_motor_set_speed(WRITE_MOTOR, sign * SPEED, 1);
    while (sign * nxt_motor_get_count(WRITE_MOTOR) <= WRITE_REV) {
        /* do nothing */
    }
    nxt_motor_set_speed(WRITE_MOTOR, 0, 1);
    nxt_motor_set_count(WRITE_MOTOR,
                        nxt_motor_get_count(WRITE_MOTOR) % WRITE_REV);
}

Writing operation is simple. It flips the bit on the tape based on the output value – clockwise to write 0 and counter-clockwise to write 1. The constant WRITE_REV is defined to be 180.

1.4 Tape Mover

1
2
3
4
5
6
7
8
9
10
11
void move(_Bool dir)
{
    int sign = dir == RIGHT ? 1 : -1;
    nxt_motor_set_speed(TAPE_MOTOR, sign * TAPE_MOV_SPEED, 1);
    while (sign * nxt_motor_get_count(TAPE_MOTOR) <= TAPE_MOVE_REV) {
        /* do nothing */
    }
    nxt_motor_set_speed(TAPE_MOTOR, 0, 1);
    nxt_motor_set_count(TAPE_MOTOR,
                        nxt_motor_get_count(TAPE_MOTOR) % TAPE_MOVE_REV);
}

move function is similar to write. Based on the given argument dir – which is either LEFT or RIGHT, it rotates the motor to move the tape to the given direction. The constant TAPE_MOVE_REV is set to 1800 (five cycles).

Limitations

This implementation works well, however, there are limitations of this implementation.

  • Single-task with polling : We have one big monolithic task doing every operation – read/write/move – in it. It uses busy-wait polling to control motors as the following code (part of move function).
1
2
3
   while (sign * nxt_motor_get_count(TAPE_MOTOR) <= TAPE_MOVE_REV) {
      /* do nothing */
   }

Problem: It wastes CPU cycles and prevent us from doing other tasks. We are going to improve this by implementing multi-task version.

  • Controlled by a Transition Relation : In this implementation, we need to provide a transition relation to program the machine. For example, the unary addition program has the following transition relation:
State Input   Output Next State Direction
0 0   0 0 L
0 1   1 1 L
1 0   1 2 L
1 1   1 1 L
2 0   0 3 R
2 1   1 2 L
3 0     ERROR  
3 1   0 4 R
4 0     HALT  
4 1   1 4 R

This form is difficult to understand and maintain. We will introduce an assembly-like language to program the machine. With the new language, we may program the unary addition as follows:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
/* Before it meets the first ones */
0:  READ
    CJUMP1 1
    MOVE   L
    JUMP   0

/* scanning first operand */
1:  MOVE   L
    READ
    CJUMP1 1
    WRITE  1
    MOVE   L

/* scanning second operand */
2:  READ
    CJUMP0 3
    MOVE   L
    JUMP   2

/* last position */
3:  MOVE   R
    READ
    CJUMP0 ERR
    WRITE  0

/* computation finished, keep moving to the right until it ends */
4:  MOVE   R
    READ
    CJUMP1 4
    HALT

ERR:
    ERROR
  • Serialized Movement: In the current implementation, Read/Write/Move operations occur one after another, even if it is physically possible to do them simulataneously in some cases. For example, the read header can start to move to the tape while the tape is being moved to the next position. The only constraint here is that the tape should not move when the colorsensor reads the value. By the same argument, we may move the writer lever and the read header simulataneously. However, we should be careful to avoid any physical collision. To implement concurrent movements, it is natural to program using multiple tasks. This extension will introduce more complexity to an implementation. We will see how to use our verification tool to make sure that an implementation has desired properties.
  • No Logging : Currently, we do not have any logging feature so that it is difficult to check the internal status of the machine or debug a program. We will start to add logging by using the LCD display in the NXT brick. Then, we will use USB communication to output log messages to the connected computer.

Install nxtOSEK in OSX Lion

There are two posts on how to install nxtOSEK in OSX (Lion) – nxtOSEK official documentation and Augusto Ribeiro’s post. However, they do not work for me. I spent some time to figure out problems and find a solution. Here is my finding:

  • Installing LEGO Fantom driver for Mac OS
  • Downloading GNU ARM toolchain
    • Note: This is version 4.6.2, not the latest version 4.7.1. I tried the latest one, however, it generated incorrect binaries which displayed broken strings once I ran them.
  • Installing GNU ARM toolchain
    • Create directory work in home folder.
    • Mount downloaded .dmg file.
    • Move installer yagarto-4.6.2 from .dmg to ~/work.
    • Run installer. It will create directory ~/work/yagarto-4.6.2 and install toolchain to it.
  • Download and install Wine via Homebrew

      brew install wine
    
  • Installing nxtOSEK
  • Editing tool_gcc.mak to specify GNU ARM directory and target prefix in ecrobot.mak
nxtOSEK/ecrobot/tool_gcc.mak
1
2
3
4
5
6
...
GNUARM_ROOT = /Users/[your_home_dir]/work/yagarto-4.6.2
...

TARGET_PREFIX :=arm-none-eabi
...
  • Editing ecrobot.mak to specify WINECONSOLE. If you use c++ instead of c, you may need to edit ecrobot++.mak
nxtOSEK/ecrobot/ecrobot.mak
1
2
3
4
5
6
7
8
# Detect OS name 
...
UNAME := $(shell uname)
ifeq ($(UNAME), Darwin)
        # Mac OS X detected.
        WINECONSOLE := LANG=en_US.UTF-8 wineconsole
        LAUNCHER := $(WINECONSOLE)
...
  • Download native nexttool for Mac OS X

  • Re-building nxtOSEK libraries

    • Go to nxtOSEK/ecrobot/c++ and run:

       make all
       make release
      
    • Go to nxtOSEK/ecrobot/c and run:

       make all
       make release
      
    • Go to nxtOSEK/ecrobot/bios and run:

       make all
       make release
      
    • Go to nxtOSEK/ecrobot/nxtway_gc_balancer and run:

       make all
       make release
      

Building a LEGO Turing Machine

In this article, I illustrate how to build a (slightly) modified version of the LEGO Turing machine built by researchers at CWI.

LEGO Turing Machine

Introduction

Internship

A month ago, I started my summer internship at Software Engineering Institute, Carnegie Mellon working on verification of concurrent programs with Dr. Arie Gurfinkel and Dr. Sagar Chaki. We looked for an interesting example to demonstrate our verification tool and to learn how we can imporve it.

LEGO Mindstorms & nxtOSEK

Interestingly, Arie and Sagar have used concurrent programs written for LEGO Mindstorm as benchmarks of their verification tool. At first time, I got an impression that these LEGO programs are not realistic. However, I learned that I was wrong.

  1. Those LEGO Mindstorms programs are running on the nxtOSEK platform.
  2. A part of nxtOSEK is TOPPERS/ATK, which provided real-time multi tasking features proven in automotive industry.
  3. Actually, OSEK in “nxtOSEK” is an open standard for automotive embedded systems, published by a consortium founded by the automobile industry including BMW, Robert Bosch GmbH, DaimlerChrysler, Opel, Siemens, Volkswagen Group, Renault and PSA Peugeot Citroën.
  4. nxtOSEK’s real-time kernel is also compatible with μITRON 4.0 specification which is a de-facto industry standard in the embedded systems field.

Mindstorms Car

Sometimes, things are more than what we see. This Mindstorms car looks like a toy, however it contains a complex embedded system inside.

CWI Turing Machine

After spending some time on searching for good examples, I found this fascinating Turing machine which was designed by researchers at CWI. I do recommend their [Video] if you have not watched it yet.

Lego Turing Machine by CWI researchers

We decided to build this machine because of the following reasons:

  • Simple Mechanics: All operations – reading, writing, and moving – can be done by simply rotating motors and reading a sensor. We do not need to worry about complex movements which are basically not our interest.
  • Inherent Parallelism: Though the CWI TM is a single-thread program, it is natural to program a Turing machine using multiple threads.

0. Required Components

  1. LEGO Mindstorms NXT 2.0 Kit (8547) ($280): Definitely, we need this one. This kit consists of one NXT brick, three servo motors, and four sensors (ultrasonic sensor, 2 touch sensors, and color sensor). To build this TM, we are going to use three servo motors and one color sensor.
    LEGO MINDSTORMS NXT
  2. Technic Parts ($20): It is not clear what components you really need even after reading the CWI webpage. They just mention that you need some other parts from LEGO Technic Kits. Watching their video several times, I figured out what we needed to build a machine with a 16-bit long tape.
Number Name Quantity
3647 Technic Gear 8 Tooth 5
3713 Technic Bush 40
3743 Technic Gear Rack 1 x 4 10
3737 Technic Axle 8 10
4274 Technic Pin 1/2 25
4716 Technic Gear Worm 2
6536 Technic Cross Block 1 x 2(Axle/Pin) 15
32014 Technic Angle Connector #6 (90 degree) (BLACK!) 15
48989 Technic Cross Block 1 x 3(Pin/Pin/Pin) with 4 Pins 10

Please note that you have to choose Black color when you buy 32014 Technic Angle Connector #6 (90 degree) because this part will be used as a *bit” in a tape.

1. Tape (16-bit)

Let’s build the tape first. Basically, 32014 Technic Angle Connector #6 (90 degree) – the L-shaped black part – plays the role of “bit”. Two bits are separated by either a 3713 Technic Bush – Red cylindrical object – or 6536 Technic Cross Block 1 x 2(Axle/Pin).

Tape #1

Tape #2

The bottom of the tape is not shown on the Video and it is actually quite tricky to figure out what there is. As you see in image 7 and 8, there are 3743 Technic Gear Rack 1 x 4 at the bottom of the tape, which are attached with 4274 Technic Pin 1/2.

2. Rail & Bridge

Rail & Bridge

Building a rail and a bridge is not difficult. Make sure that the gap in the rail is three-hole wide so that the tape can fit in it.

3. Engine (Gears & Gear Worms)

This is the most interesting part of the machine. Here is a problem. We need linear movement to move the tape back and forth while our servo motor only provides circular movement. The CWI design solves this problem by using gear, gear worms, and gear racks.

My solution is simpler than the CWI design in a sense that mine does not use a bevel gear.

Engine #1

Note that there are some inconsistencies between picture #4 and #6 (Thanks to Serj Smorod). There are two grey upper bricks on the left side (#4) and on the right (#6). You should take #4.

Once you finish up to step 6, please make sure that the gear worms do not move back and forth when you rotate the 24-teeth black gear.

Engine #2

You also need to place additional 3647 Technic Gear 8 Tooth on the rail to hold the tape stably (see the top and bottom parts of Engine #2 image).

4. Tape Mover

We need to transfer the drive from a motor to the engine part. First assemble the Tape Mover unit with a servo motor.

Tape Mover

Then attach it to the bridge and engine part. Make sure that there is no movement of the motor when it runs.

Attached Tape Mover

5. Reader

Reader

The Reader unit consists of one servo motor and one color sensor. Once you assemble it, attach to the rail & bridge.

Attached Reader

6. Writer

Writer

The Writer unit has a servo motor with a lever to flip a bit. It is important to align the Reader and Writer well so that they can read and write the same bit of the tape.

Attached Writer

That’s it!

Once you finish all the steps, connect all the motors and the sensor to the NXT brick using cables. Now, you are ready to run this machine!

Lego Turing Machine