Luận văn Tính cận trên bộ nhớ log của chương trình sử dụng giao dịch
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƢỜNG ĐẠI HỌC CÔNG NGHỆ
NGUYỄN PHAN TÌNH
TÍNH CẬN TRÊN BỘ NHỚ LOG CỦA CHƢƠNG
TRÌNH SỬ DỤNG GIAO DỊCH
LUẬN VĂN THẠC SỸ CÔNG NGHỆ THÔNG TIN
Hà Nội - 2016
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƢỜNG ĐẠI HỌC CÔNG NGHỆ
NGUYỄN PHAN TÌNH
TÍNH CẬN TRÊN BỘ NHỚ LOG CỦA CHƢƠNG
TRÌNH SỬ DỤNG GIAO DỊCH
Ngành:
Chuyên ngành: Kỹ thuật Phần Mềm
Mã số: 60480103
Công Nghệ Thông Tin
LUẬN VĂN THẠC SỸ CÔNG NGHỆ THÔNG TIN
NGƢỜI HƢỚNG DẪN KHOA HỌC: PGS.TS. Trƣơng Anh Hoàng
Hà Nội - 2016
LỜI CAM ĐOAN
Tôi xin cam đoan luận văn này là do tôi thực hiện, đƣợc hoàn thành dƣới sự
hƣớng dẫn trực tiếp từ PGS.TS.Trƣơng Anh Hoàng. Các trích dẫn có nguồn gốc rõ
ràng, tuân thủ tôn trọng quyền tác giả. Luận văn này không sao chép nguyên bản từ bất
kì một nguồn tài liệu nào khác.
Nếu có gì sai sót, tôi xin chịu mọi trách nhiệm.
Học viên
Nguyễn Phan Tình
1
LỜI CẢM ƠN
Để hoàn thành đề tài luận văn này bên c nh sự chủ động cố gắng của bản th n
tôi đ nhận đƣợc sự ủng hộ và gi p đ nhiệt t nh từ c c tập thể c nh n trong và ngoài
trƣờng.
Qua đ y cho phép tôi đƣợc bày t l ng cảm ơn s u sắc tới thầy PGS.TS.Trƣơng
Anh Hoàng giảng viên trƣờng Đ i học công nghệ – Đ i học Quốc gia Hà Nội ngƣời
đ trực tiếp động viên định hƣớng và hƣớng dẫn tận t nh trong qu tr nh học tập và
hoàn thành đề tài luận văn này.
Đồng k nh g i lời cảm ơn đến tập thể c c thầy cô gi o trong trƣờng Đ i học
Công Nghệ – Đ i học Quốc gia Hà Nội đ trau dồi kiến thức cho tôi điều đ là nền
tảng qu b u g p phần to lớn trong qu tr nh vận dụng vào hoàn thiện luận văn.
Cuối c ng tôi xin đƣợc g i l ng biết ơn s u sắc đến gia đ nh b n b đồng
nghiệp đ t o điều kiện về vật chất c ng nhƣ tinh thần luôn s t c nh bên tôi động
viên gi p tôi yên t m học tập và kết th c kh a học.
Tôi xin ch n thành cảm ơn
2
MỤC LỤC
LỜI CẢM ƠN.........................................................................................................2
DANH MỤC CÁC BẢNG .....................................................................................7
DANH MỤC CÁC HÌNH VẼ ................................................................................7
MỞ ĐẦU ................................................................................................................8
Tính cấp thiết của đề tài......................................................................................8
Mục tiêu nghiên cứu ...........................................................................................8
Phƣơng ph p nghiên cứu ....................................................................................9
Cấu trúc của luận văn .........................................................................................9
1.1. Giới thiệu ...................................................................................................10
1.2. Hƣớng tiếp cận...........................................................................................11
1.3. Ví dụ minh họa ..........................................................................................11
2.1. Hệ thống kiểu.............................................................................................14
2.1.1. Giới thiệu về hệ thống kiểu.................................................................14
2.2.1. Giao dịch (Transaction) ......................................................................18
3.1. Cú pháp của TM [1]...................................................................................21
3.2. Các ngữ nghĩa động...................................................................................21
3.2.1. Ngữ nghĩa cục bộ................................................................................21
4.1. Các kiểu .....................................................................................................24
4.2. Các quy tắc kiểu.........................................................................................27
5.2.2. Thuật toán Cộng (Joint)......................................................................33
5.2.3. Thuật toán gộp (Merge)......................................................................34
5.2.4. Thuật toán JoinCommit ......................................................................37
KẾT LUẬN...........................................................................................................50
TÀI LIỆU THAM KHẢO ....................................................................................51
4
DANH MỤC CÁC KÝ HIỆU, THUẬT NGỮ, CHỮ VIẾT TẮT
CHỮ VIẾT TẮT, THUẬT
GIẢI NGHĨA
STT
NGỮ, KÝ HIỆU
CHỮ VIẾT TẮT
TM
–
Transactional Ngôn ngữ để viết chƣơng tr nh giao dịch
1
2
Memory
STM
-
Software Bộ nhớ giao dịch phần mềm, một giải pháp viết
Transactional Memory
c c chƣơng tr nh song song
THUẬT NGỮ
1
Type System
Transaction
Hệ thống kiểu
2
Giao dịch
3
illegal memory reference
Data corruption
Thread
Tham chiếu bộ nhớ không hợp lệ
Hƣ h ng dữ liệu
4
5
Luồng
6
Type checker
Type checking
Well-behaved
Well-formed
Ill-behaved
Bộ kiểm tra kiểu
7
Trình kiểm tra kiểu
8
Tính chất hành x đ ng của chƣơng tr nh.
Tính chất thiết lập đ ng của chƣơng tr nh.
Tính chất hành x yếu của chƣơng tr nh.
Định kiểu tốt.
9
10
11
12
13
14
19
20
21
22
23
24
25
26
27
Well-typed
Ill-typed
Định kiểu yếu.
ADT-Abstract Data Type
Illegal instruction
Atomicity
Kiểu dữ liệu trừu tƣợng
Lệnh không hợp lệ
Tính nguyên t
Consistency
Isolation
Tính nhất quán
T nh độc lập
Durability
Tính bền vững
Onacid
Tr ng thái mở một giao dịch
Tr ng thái kết thúc một giao dịch
Các giao dịch lồng
Commit
Nested transactions
Multi-threaded
Spawn
Đa luồng
Sinh luồng
Joint commits
Các commit của các luồng song song đồng thời
thực hiện kết thúc một giao tác chung.
Ngữ nghĩa cục bộ
28
29
30
31
32
Local semantics
Global semantics
Local enviroments
Global enviroments
Ngữ nghĩa toàn cục
Môi trƣờng cục bộ
Môi trƣờng toàn cục
5
33
Syntax
+n
Cú pháp
KÝ HIỆU
Mô tả thành phần + trong hệ thống kiểu dựa trên
chuỗi số có dấu, mở giao dịch c k ch thƣớc là n
đơn vị bộ nhớ
1
2
3
4
-
n
Mô tả thành phần – trong hệ thống kiểu dựa trên
chuỗi số có dấu, m thao tác commit liên tiếp.
Mô tả thành phần # trong hệ thống kiểu,chỉ ra số
đơn vị bộ nhớ lớn nhất đƣợc s dụng bởi thành
phần là n.
#n
¬n
Mô tả thành phần ¬ thể hiện số luồng c ng đồng
bộ t i một thời điểm joint commits
6
DANH MỤC CÁC BẢNG
Bảng 3.1 Bảng cú pháp của TM ...........................................................................21
Bảng 3.2. Bảng ngữ nghĩa động của TM..............................................................23
Bảng 4.1 Các quy tắc kiểu ....................................................................................27
DANH MỤC CÁC HÌNH VẼ
H nh 1.1 Đo n mã cho mô hình giao dịch lồng và đa luồng ................................11
Hình 1.2 Mô hình giao dịch lồng và đa luồng......................................................12
Hình 2.1 Hệ thống kiểu trong trinh biên dịch.......................................................17
Hình 2.2 Các tr ng thái của giao dịch...................................................................18
Hình 4.1 Các luồng song song Joincommit..........................................................28
Hình 5.1 Hình mô tả c c giai đo n tính cận trên tài nguyên bộ nhớ log..............40
Hình 5.2 Mô hình giao dịch lồng và đa luồng cho ví dụ 5.1 ................................41
Hình 5.3 Mô tả giai đo n 1 của thuật toán tính tài nguyên...................................41
Hình 5.4 Mô hình giao dịch lồng và đa luồng cho thực nghiệm 1 .......................45
Hình 5.5 Màn hình kết quả thực nghiệm 1 ...........................................................45
Hình 5.6 Mô hình giao dịch lồng và đa luồng cho thực nghiệm 2 .......................46
Hình 5.7 Màn hình kết quả thực nghiệm 2 ...........................................................46
Hình 5.8 Mô hình giao dịch lồng và đa luồng cho thực nghiệm 3 .......................47
Hình 5.9 Màn hình kết quả ch y thực nghiệm 3...................................................47
Hình 5.10 Mô hình giao dịch cho thực nghiệm 4.................................................48
Hình 5.11 Màn hình kết quả thực nghiệm 4 .........................................................48
Hình 5.12 Mô hình giao dịch lồng và đa luồng cho thực nghiệm 5 .....................49
Hình 5.13 Màn hình kết quả thực nghiệm 5 .........................................................49
7
MỞ ĐẦU
Tính cấp thiết của đề tài
Cùng với sự phát triển nhƣ v b o của khoa học công nghệ, các vi x lý hiện đ i
ngày càng thể hiện sức m nh qua nhiều nhân (core) với tốc độ x lý ngày càng cao. Có
đƣợc nhƣ vậy là do bên trong các vi x lý này đƣợc thiết kế các luồng (thread) có khả
năng ch y và x lý song song. Trƣớc đ y để lập trình đa luồng, ngƣời ta s dụng cơ
chế đồng bộ (synchronization) dựa trên kh a (lock) để p đặt giới h n về quyền truy
cập tài nguyên trong một môi trƣờng khi có nhiều luồng thực thi.Tuy nhiên, khi áp
dụng phƣơng ph p này thƣờng nảy sinh các vấn đề nhƣ khóa chết (deadlock) hoặc các
lỗi tiềm tàng…
Software Transactional Memory (STM- bộ nhớ giao dịch phần mềm) [8] là một
giải ph p đơn giản hơn nhƣng vô c ng m nh mẽ mà có thể giải quyết đƣợc hầu hết
các vấn đề trên. N đ thay thế hoàn toàn giải ph p c trong việc truy cập bộ nhớ dùng
chung. STM giao tiếp với bộ nhớ thông qua các giao dịch. Các giao dịch này cho phép
tự do đọc ghi để chia sẻ các biến và một vùng nhớ gọi là log sẽ đƣợc s dụng để ghi
l i các ho t động này cho tới khi kết thúc giao dịch.
Một trong những mô hình giao dịch phức t p s dụng STM là mô hình giao dịch
lồng và đa luồng (nested and multi-threaded transaction) [5]. Trong quá trình thực thi
của c c chƣơng tr nh giao dịch lồng và đa luồng, khi các luồng mới đƣợc sinh ra hoặc
một giao dịch đƣợc bắt đầu, các vùng bộ nhớ gọi là log sẽ đƣợc cấp phát. Các log này
d ng để lƣu l i bản sao của các biến dùng chung, nhờ vậy mà các luồng trên có thể s
dụng các biến này một c ch độc lập.
Vấn đề đặt ra ở đ y là t i thời điểm chƣơng tr nh ch y liệu lƣợng bộ nhớ cần cấp
ph t cho c c log c vƣợt quá tài nguyên bộ nhớ của máy, hay chƣơng tr nh c thể ch y
một c ch trơn tru mà không gặp phải bất kỳ lỗi nào nhƣ hết bộ nhớ. Chính vì vậy, việc
x c định cận trên của bộ nhớ ở thời điểm ch y chƣơng tr nhcủa chƣơng tr nh giao dịch
là một vấn đề then chốt c ý nghĩa hết sức quan trọng.
Chính v l do đ trong luận văn thực hiện ở đ y một nghiên cứu s dụng
phƣơng ph p ph n t ch tĩnh để giải quyết bài toán tính cận trên bộ nhớ log của chƣơng
trình có giao dịch sẽ đƣợc trình bày, dựa trên bài báo đ đƣợc các tác giả công bố
trong [1].
Mục tiêu nghiên cứu
Luận văn đƣợc thực hiện dựa trên nghiên cứu trong bài báo [1]. Do vậy để có thể
hiểu đƣợc giải pháp các tác giả đ đề xuất trong [1], trong luận văn này tập trung
nghiên cứu các lý thuyết về hệ thống kiểu; Các khái niệm cơ bản c ng nhƣ t nh chất
của giao dịch; Nghiên cứu cú pháp và ngữ nghĩa của ngôn ngữ TM (Transactional
Memory) – Một ngôn ngữ để viết các chƣơng tr nh giao dịch. Từ việc nắm đƣợc giải
pháp xây dựng hệ thống kiểu đề cập trong bài báo, một công cụ sẽ đƣợc cài đặt dựa
trên ngôn ngữ C#.
8
Phƣơng pháp nghiên cứu
Để thực hiện đƣợc mục tiêu đ đề ra trong luận văn c c phƣơng ph p nghiên cứu
sau đ y đ đƣợc kết hợp:
- Phƣơng ph p nghiên cứu lý thuyết: bao gồm phân tích, tổng hợp các tài liệu, bài
báo có liên quan về lý thuyết hệ thống kiểu đặc biệt là hệ thống kiểu cho c c chƣơng
trình TM, tài liệu về các thuật toán dựa trên hệ thống kiểu..
- Phƣơng ph p thực nghiệm: Cài đặt thuật to n đ đề xuất, ch y th để kiểm tra
t nh đ ng đắn của chƣơng tr nh.
Cấu trúc của luận văn
Luận văn đƣợc trình bày trong các phần, với nội dung chính của mỗi phần nhƣ
sau:
Mở đầu: Nêu ra tính cấp thiết của đề tài, nêu ra các mục tiêu cần nghiên cứu, các
phƣơng ph p đƣợc s dụng khi nghiên cứu và cấu trúc các phần của luận văn.
Chƣơng 1: Giới thiệu bài toán
Trình bày nội dung cụ thể của bài toán tính cận trên bộ nhớ log của chƣơng tr nh
có s dụng giao dịch, các vấn đề cần giải quyết trong bài to n này và hƣớng tiếp cận
để giải quyết bài toán. Trong phần này, c c điểm cải tiến của phƣơng ph p giải quyết
bài toán ở đ y so với c c phƣơng ph p trƣớc kia c ng đƣợc nêu ra. Ví dụ đƣợc trình
bày trong mục 1.3 sẽ minh họa rõ ràng cho bài to n và hƣớng tiếp cận đ đƣa ra.
Chƣơng 2: Một số kiến thức cơ sở
Trình bày các lý thuyết cơ bản đƣợc s dụng làm cơ sở để giải quyết bài toán,
bao gồm: Lý thuyết về hệ thống kiểu nhƣ kh i niệm, các thuộc tính hay ứng dụng của
hệ thống kiểu trong thực tế; Lý thuyết về giao dịch, bộ nhớ giao dịch phần mềm gồm
các khái niệm, tính chất, ứng dụng…
Chƣơng 3: Ngôn ngữ giao dịch
Giới thiệu ngôn ngữ giao dịch TM (Transactional memory)- Một ngôn ngữ đƣợc
d ng để viết c c chƣơng tr nh giao dịch. Trong chƣơng này cú pháp và ngữ nghĩa của
ngôn ngữ TM sẽ đƣợc trình bày cụ thể.
Chƣơng 4: Hệ thống kiểu cho chƣơng trình giao dịch
Nghiên cứu hệ thống kiểu để giải quyết bài toán tính cận trên bộ nhớ log cho
chƣơng tr nh c giao dịch đ đƣợc trình bày trong bài báo [1]. Lý thuyết hệ thống kiểu
đƣợc phát triển ở đ y bao gồm các kiểu và các quy tắc kiểu.
Chƣơng 5: Xây dựng công cụ và thực nghiệm
Cài đặt các thuật toán kiểu dựa trên hệ thống kiểu đ đƣợc trình bày ở chƣơng 4.
Từ các thuật to n đ xây dựng công cụ để giải quyết bài toán tính cận trên bộ nhớ log
và thực nghiệm để kiểm tra t nh đ ng đắn của công cụ.
Kết luận:
Đ nh gi c c kết quả đ đ t đƣợc, nêu ra tồn t i và hƣớng phát triển.
9
CHƢƠNG 1. GIỚI THIỆU BÀI TOÁN
1.1. Giới thiệu
Nhƣ ch ng ta đ đề cập ở phần mở đầu, STM là giải ph p đƣợc s dụng trong
việc chia sẻ bộ nhớ dùng chung và một trong những mô hình giao dịch phức t p s
dụng STM là mô hình giao dịch lồng và đa luồng (nested and multi-threaded
transaction)
Ở đ y một giao dịch đƣợc gọi là lồng khi nó chứa một số giao dịch khác. Chúng
ta gọi giao dịch c là giao dịch cha và gọi các giao dịch mà sinh ra trong giao dịch cha
là giao dịch con. Các giao dịch con này phải đƣợc đ ng trƣớc giao dịch cha. Hơn nữa,
giao dịch đƣợc gọi là đa luồng (multi-threaded) khi các luồng con sinh ra đƣợc ch y
bên trong giao dịch đồng thời ch y song song với luồng cha đang thực thi giao dịch.
Khi một giao dịch đƣợc bắt đầu một vùng bộ nhớ gọi là log đƣợc cấp phát d ng để lƣu
l i bản sao của các biến dùng chung. Một luồng mới hay luồng con khi đƣợc sinh ra
c ng sẽ t o một bản sao các log giao dịch của luồng cha. Khi luồng cha thực hiện đ ng
(commit) giao dịch, tất cả các luồng con đƣợc t o bên trong luồng cha phải c ng đ ng
với luồng cha. Chúng ta gọi kiểu đ ng này là join commit, và thời điểm khi những
commit này xảy ra đƣợc gọi là thời điểm joint commit. Ở thời điểm join commit bộ
nhớ đƣợc cấp ph t cho c c log c ng đƣợc giải phóng. Join commit đ ng vai tr nhƣ sự
đồng bộ ngầm của các luồng song song. Chính vì hình thức đồng bộ này mà các luồng
song song bên trong một giao dịch không hoàn toàn ch y độc lập.
Và vấn đề cần trả lời ở đ y là liệu ở thời điểm ch y chƣơng tr nh, liệu lƣợng bộ
nhớ cần cấp ph t cho c c log c vƣợt quá tài nguyên bộ nhớ của máy hay chƣơng
trình có thể ch y một c ch trơn tru mà không gặp phải bất kỳ lỗi nào nhƣ hết bộ nhớ.
Để trả lời cho câu h i này, chúng ta cần phải x c định đƣợc biên bộ nhớ của chƣơng
trình giao dịch hay chính là cận trên bộ nhớ đƣợc cấp phát cho các log ở thời điểm
biên dịch.
Ở các nghiên cứu trƣớc đ y [2, 11], một hệ thống kiểu đƣợc phát triển để đếm số
lƣợng log lớn nhất mà cùng tồn t i ở một thời điểm khi chƣơng tr nh đang ch y. Con
số này chỉ cho thông tin thô về bộ nhớ đƣợc s dụng bởi các log giao dịch. Để quyết
định thêm ch nh x c lƣợng bộ nhớ lớn nhất mà các log giao dịch có thể s dụng, trong
nghiên cứu [1] các tác giả đ đề xuất phƣơng ph p giải quyết vấn đề với việc t nh đến
k ch thƣớc của mỗi log. Đ y c ng là điểm cải tiến của hƣớng tiếp cận mới này so với
c c hƣớng tiếp cận trƣớc đ .
Nhƣ vậy, bài toán cần giải quyết ở đ y c thể phát biểu nhƣ sau: T nh to n lƣợng
bộ nhớ yêu cầu lớn nhất cho toàn bộ chƣơng tr nh giao dịch khi biết k ch thƣớc của
các log.
10
1.2. Hƣớng tiếp cận
Để giải quyết bài to n đặt ra trƣớc hết chúng ta sẽ viết c c chƣơng tr nh giao
dịch bằng một ngôn ngữ dành riêng cho nó, cụ thể là ngôn ngữ TM sẽ đƣợc trình bày
trong chƣơng 3.
Để thêm thông tin về k ch thƣớc của mỗi log, chúng ta sẽ mở rộng lệnh bắt đầu
giao dịch trong các nghiên cứu trƣớc để chứa thông tin này. Sau đ chúng ta phát triển
một hệ thống kiểu để đ nh gi tài nguyên bộ nhớ log mà các giao dịch có thể yêu cầu.
So với các nghiên cứu trƣớc [2,11] th ý tƣởng về các cấu trúc kiểu trong nghiên
cứu [1] không có g thay đổi. Tuy nhiên, các ngữ nghĩa kiểu và các quy tắc kiểu là mới
và khác so với các nghiên cứu trƣớc đ y.
1.3. Ví dụ minh họa
Để giải thích cho vấn đề và hƣớng tiếp cận đ tr nh bày trên ch ng ta sẽ xem xét
một ví dụ, đƣợc mƣợn từ [1]. Trong ví dụ này chúng ta chỉ tập trung vào lõi của ngôn
ngữ mà không quan tâm tới các cấu trúc khác ở một chƣơng tr nh thật sự nhƣ c c thủ
tục, c c phƣơng thức gọi, truyền thông điệp, các biến và c c t nh to n cơ bản…
Hình 1.1 Đoạn mã cho mô hình giao dịch lồng và đa luồng
Trong đo n mã ở trên, lệnh onacid và commit là các lệnh bắt đầu và đ ng một
giao dịch [8]. Lệnh spawn là lệnh t o ra một luồng mới với m đƣợc thể hiện bởi các
tham số của lệnh. Lệnh onacid trong các nghiên cứu trƣớc đ y không c tham số,
nhƣng trong nghiên cứu này nó liên kết với một số để ký hiệu k ch thƣớc của bộ nhớ
cần đƣợc cấp phát cho log của giao dịch ở thời điểm thực thi.
Các hành vi của chƣơng tr nh này đƣợc miêu tả trong hình 1.2
11
Hình 2.2 Mô hình giao dịch lồng và đa luồng
Trong đ :
onacid : Lệnh bắt đầu giao dịch, ký hiêu bởi [
commit: Lệnh kết thúc giao dịch, bởi dấu ].
Lệnh spawn t o ra một luồng mới ch y song song với luồng cha của n và đƣợc
mô tả bằng đƣờng kẻ ngang. Luồng mới sao chép các log của luồng cha cho việc lƣu
một bản sao giá trị các biến của luồng cha để nó có thể dùng các biến này một cách
độc lập.
Trong hình vẽ trên các joint commit thể hiện thời điểm các luồng cha, con cùng
đồng bộ đƣợc thể hiện bằng hình chữ nhật nét đứt c c điểm đồng bộ này đƣợc đ nh
dấu bằng c nh bên phải của hình chữ nhật.
Sau đ y ch ng ta sẽ thực hiện tính tài nguyên bộ nhớ cho chƣơng tr nh trong
hình 1.2 t i 3 thời điểm kh c nhau đƣợc chia ra theo các phân vùng độc lập 1, 2 và 3
nhƣ h nh vẽ.
Ta thấy t i phân vùng 1, thì bộ nhớ log dành cho luồng 0 là1+2+3= 6 đơn vị bộ
nhớ; Bộ nhớ log dành cho luồng 1 là (1+2)+4 = 7 đơn vị bộ nhớ, và Bộ nhớ log dành
cho luồng 2 là (1+2)+3+5= 11 đơn vị bộ nhớ. Nhƣ vậy ở thời điểm này, tổng tài
nguyên bộ nhớ đƣợc s dụng là 6+7+11=24 đơn vị bộ nhớ.
T i phân vùng 2, bộ nhớ log dành cho luồng 0 là 1+2+6=9 đơn vị bộ nhớ, bộ
nhớ log dành cho luồng 1 là (1+2)= 3 đơn vị bộ nhớ; Và bộ nhớ log dành cho luồng 2
là (1+2) = 3 đơn vị bộ nhớ. Do đ tổng tài nguyên bộ nhớ ở thời điểm 2: 9+3+3= 15;
T i ph n v ng 3 ta t nh đƣợc bộ nhớ log dành cho luồng 0 là 1+7= 8 đơn vị bộ
nhớ, luồng 1 là 1 và luồng 2 là 1 đơn vị bộ nhớ. Do đ tổng tài nguyên bộ nhớ cho
phân vùng 3 là 8+1+1=10 đơn vị bộ nhớ.
Nhƣ vậy tổng tài nguyên tổng hợp cho cả mô hình này phải là giá trị lớn nhất
của tài nguyên t i các phân vùng, và giá trị thu đƣợc ở đ y là 24.
Chúng ta thấy rằng trong các nghiên cứu [2,10,11] tài nguyên đƣợc ƣớc tính bởi
số giao dịch mở nhiều nhất hay số log lớn nhất mà cùng tồn t i ở thời điểm chƣơng
tr nh đang ch y.
12
Nhƣ ch ng ta thấy trong ví dụ này th lƣợng bộ nhớ yêu cầu cho các log đ t tới
có thể khác so với kết quả khi tính số lƣợng log lớn nhất đ t đƣợc trong các nghiên
cứu nhƣ [2 11] (c ng v dụ trên nhƣng trong nghiên cứu [11] thì kết quả là 11).
13
CHƢƠNG 2. MỘT SỐ KIẾN THỨC CƠ SỞ
2.1. Hệ thống kiểu
2.1.1. Giới thiệu về hệ thống kiểu
Về định nghĩa hệ thống kiểu c rất nhiều quan điểm đƣợc đƣa ra. Trong c c
ngôn ngữ lập tr nh hệ thống kiểu đƣợc định nghĩa là tập c c quy tắc để g n thuộc t nh
đƣợc gọi là kiểu cho các cấu trúc của một chƣơng tr nh m y t nh bao gồm các biến,
biểu thức, các hàm, hoặc module...Theo lý thuyết ngôn ngữ, một hệ thống kiểu là một
tập các quy tắc quy định cấu trúc và lập luận cho ngôn ngữ. Trong lập trình, hệ thống
kiểu đƣợc định nghĩa là một cơ chế c ph p ràng buộc cấu tr c của chƣơng tr nh bằng
việc kết hợp c c thông tin ngữ nghĩa với c c thành phần trong chƣơng tr nh và giới h n
ph m vi của c c thành phần đ .
Mục đ ch cơ bản của hệ thống kiểu là ngăn chặn c c sự cố do c c lỗi thực thi
trong qu tr nh chƣơng tr nh ch y [3, 6]. N đƣợc thực hiện bằng c ch định nghĩa c c
giao diện giữa các phần khác nhau của một chƣơng tr nh m y t nh và sau đ kiểm tra
xem các thành phần đ đƣợc ghép nối nhất qu n hay chƣa. Việc kiểm tra này có thể
xảy ra tĩnh (t i thời gian biên dịch), hoặc động (t i thời gian ch y), hoặc kết hợp cả
kiểm tra tĩnh và động. Ngoài ra hệ thống kiểu c n đƣợc s dụng với nhiều mục đ ch
khác, chẳng h n nhƣ cho phép tối ƣu h a tr nh biên dịch nhất định, cung cấp một hình
thức tài liệu…
Một hệ thống kiểu liên kết một kiểu với mỗi giá trị tính toán, bằng cách kiểm
tra luồng (flow) của các giá trị, nỗ lực để đảm bảo hoặc chứng minh rằng không có lỗi
kiểu có thể xảy ra.
Một trong những dấu hiệu của lỗi thực thi là lỗi phần mềm. Chẳng h n lỗi c
thể là lệnh sai (illegal instruction), tham chiếu bộ nhớ sai luật (illegal memory
reference) hoặc hƣ h ng dữ liệu (data corruption).
Một biến c thể c một miền gi trị trong suốt thời gian ch y chƣơng tr nh. Kiểu
của biến là cận trên của miền đ . V dụ nếu một biến x kiểu Integer, gi trị của n chỉ
đƣợc phép là c c gi trị nguyên trong bất kỳ lần thực thi nào của chƣơng tr nh. Giả s
x và y c kiểu Interger th biểu thức x/y hợp lệ trong mọi l c thực thi của chƣơng
tr nh. Ngƣợc l i nếu những biến này c kiểu String th x/y sẽ là nguyên nh n cho c c
lỗi ph t sinh kh c. C c ngôn ngữ đƣa ra c c kiểu không tầm thƣờng (non- trivial) cho
các biến đƣợc gọi là c c ngôn ngữ định kiểu.
Các ngôn ngữ không định kiểu không giới h n ph m vi gi trị của c c biến.
Tất cả c c gi trị đƣợc chứa trong một kiểu phổ qu t. V dụ về ngôn ngữ nhƣ vậy là
assembly ngôn ngữ này cho phép bất kỳ thao t c (phép tính) nào đƣợc thực hiện trên
bất kỳ dữ liệu. Dữ liệu trong c c ngôn ngữ đ đƣợc coi nhƣ khối c c bit.
Một hệ thống kiểu trong một ngôn ngữ định kiểu theo dõi c c kiểu của c c biến
và biểu thức trong một chƣơng tr nh. N x c định liệu một tiến tr nh một chƣơng trình
là hành x đ ng (well behaved) hay không. C c chƣơng tr nh nguồn đƣợc kiểm chứng
14
bởi hệ thống kiểu để x c định rằng ch ng cần đƣợc xem xét khi c c chƣơng tr nh hợp
lệ hoặc cần bị lo i b khi c c chƣơng tr nh không an toàn. Một chƣơng tr nh đƣợc cho
là an toàn nếu n không g y ra c c lỗi mà không đƣợc ch ý trong một thời gian. Nhƣ
c c lỗi sẽ g y ra hành vi t y ý (arbitrary behaviour). V dụ cho c c lỗi đ là truy cập
địa chi tr i luật (illegal address accessing) (v dụ : truy cập dữ liệu của bất kỳ mảng
nào với chỉ số nằm ngoài c c biên của mảng) nhảy tới địa chỉ sai ( v dụ bộ nhớ c
hoặc không thể biểu diễn một luồng lệnh). Ngôn ngữ định kiểu t o ra t nh an toàn bằng
c ch s dụng cả kiểm tra tĩnh hoặc cả kiểm tra động lẫn tĩnh cho tất cả chƣơng trình.
Bằng c ch s dụng kiểm tra tĩnh ngôn ngữ định kiểu kiểm tra c c chƣơng tr nh trƣớc
khi ch y ch ng (v dụ ở thời điểm compile).Mặt kh c kiểm tra động đƣợc thực hiện
khi chƣơng tr nh đang ch y. Một ngôn ngữ c thể x c định nhƣ tập c c lỗi chẳng h n
các lỗi cấm. Sau đ ngôn ngữ kiểm chứng mỗi chƣơng tr nh c là hành x đ ng (well
behaved ) hay không nếu ch ng không g y ra bất kỳ lỗi nào mà không đƣợc phép xảy
ra. Nói chung, một chƣơng tr nh hành x đ ng phải là một chƣơng tr nh an toàn . Điều
đ c nghĩa là c c lỗi không đƣợc phép phải bao gồm tất cả c c lỗi không đƣợc lƣu ý
đ đƣợc mô tả trong phần trên. Tr i ngƣợc với hành x tốt là hành x yếu (ill
behaved).
Các ngôn ngữ kiểu có thể thực hiện kiểm tra tĩnh để đảm bảo hành vi tốt và ngăn
chặn tính không an toàn và c c chƣơng tr nh hành x yếu đƣợc ch y. Quá trình kiểm
tra đƣợc gọi là trình kiểm tra kiểu (typechecking), và các thuật to n đƣợc s dụng
đƣợc gọi là bộ kiểm tra kiểu (typechecker). Chƣơng tr nh đƣợc cho là định kiểu tốt
(well typed) nếu nó có thể vƣợt qua bộ kiểm tra kiểu; Ngƣợc l i nếu không vƣợt qua,
gọi là định kiểu yếu. Java hay Pascal là các ví dụ về ngôn ngữ s dụng kiểm tra tĩnh .
Kiểm tra động là các kiểm tra trong thời gian thực thi để tìm ra tất cả các lỗi cấm.
ngôn ngữ không định kiểu s dụng kiểm tra động để thực thi hành vi tốt. Những ngôn
ngữ này có thể kiểm tra các phép toán chia, giới h n của mảng…khi lỗi xảy ra.
Để đ t đƣợc an toàn, các ngôn ngữ định kiểu có thể cần phải thực hiện các kiểm
tra trong thời gian ch y. Ví dụ, giới h n của mảng thƣờng đƣợc kiểm tra động. Đ là
trƣờng hợp khi kiểm tra động s dụng bởi một ngôn ngữ định kiểu. Vì vậy, một ngôn
ngữ đ đƣợc kiểm tra tĩnh không c nghĩa là chƣơng tr nh đƣợc thực hiện hoàn toàn
mù quáng.
Theo định nghĩa một chƣơng trình hành x tốt th c ng an toàn. Mục tiêu cơ bản
của hệ thống kiểu là để thực thi an toàn bằng cách lo i trừ tất cả các lỗi không đƣợc
chú ý trong tất cả c c chƣơng tr nh. Tuy nhiên hầu hết các hệ thống lo i này đƣợc
thiết kế m nh hơn. Ch ng đƣợc s dụng để đảm bảo thuộc tính hành x tốt, và hoàn
toàn an toàn. Hệ thống kiểu phân lo i một chƣơng tr nh nhƣ định kiểu yếu hoặc định
kiểu tốt.
Một hệ thống kiểu đƣa ra c c quy tắc kiểu cho một ngôn ngữ lập trình. Trong hệ
thống kiểu thuật toán của trình kiểm tra kiểu (typechecking) mà tƣơng ứng với các
15
định nghĩa ngôn ngữ là độc lập với trình biên dịch. Với hệ thống kiểu cùng lo i, trình
biên dịch khác nhau có thể s dụng các thuật toán kiểm tra kiểu khác nhau.
2.1.2. Các thuộc tính của hệ thống kiểu
Một hệ thống kiểu có một số thuộc tính sau:
Khả năng kiểm chứng: Hệ thống kiểu phải có thuật toán kiểm tra kiểu để phân
lo i c c chƣơng tr nh. Một hệ thống kiểu phải chủ động nắm bắt lỗi thực thi trƣớc khi
chúng xảy ra.
Tƣờng minh: Các lập trình viên có thể dự đo n nếu một chƣơng tr nh vƣợt qua
bộ kiểm tra kiểu. Nếu nó lỗi khi kiểm tra, nên t m đƣợc lí do một cách dễ dàng.
Khả năng thực thi: C c biến, biểu thức nên đƣợc kiểm tra tĩnh càng nhiều càng
tốt. Mặt kh c ch ng c ng cần đƣợc kiểm tra động. Sự nhất quán cần đƣợc kiểm chứng
một c ch thƣờng xuyên.
2.1.3. Các ứng dụng của hệ thống kiểu
Hệ thống kiểu đ ng vai tr quan trọng trong công nghệ phần mềm và trong lĩnh
vực bảo mật m ng.
Đối với công nghệ phần mềm n đƣợc s dụng trong trình biên dịch của các
ngôn ngữ lập trình, tối ƣu h a trong cơ sở dữ liệu và thậm chí là mô hình các ngôn
ngữ tự nhiên… Trong ngôn ngữ lập trình, hệ thống kiểu có các chức năng ch nh sau :
a. Phát hiện i
Khi chƣơng tr nh ch y có thể xảy ra nhiều lo i lỗi khác nhau. Có lỗi có thể tác
động tức th đến kết quả chƣơng tr nh nhƣng c những lỗi tiềm ẩn mà chỉ làm thay đổi
dữ liệu nhƣng không thấy ngay ở kết quả.
Ví dụ : Khi khai báo biến trong C#, nếu ta viết khai b o nhƣ sau:
bool x;
Trình biên dịch sẽ báo lỗi không hợp lệ vì không đƣợc phép biến khai báo mà
không khởi t o giá trị. Lỗi này sẽ dừng chƣơng tr nh ngay lập tức. Để không bị báo lỗi,
ta có thể s a khai báo trên là : bool x= true;
Hệ thống kiểu có nhiệm vụ ngăn chặn các lỗi thực thi, lỗi mà có thể xảy ra khi
ch y chƣơng tr nh. Nhƣng khi những lỗi này ở d ng tiềm tàng, hệ thống kiểu không
thể nhận ra đƣợc. Vì vậy độ ch nh x c của hệ thống kiểu phụ thuộc vào nguyên nh n
g y ra lỗi thực thi. Nó theo dõi kiểu của c c đối số và c thể tìm ra các phần m lệnh
không hợp lệ. Hệ thống kiểu c thể theo dõi sự vắng mặt của lớp nào đ do lỗi lập
trình nhờ vào khả năng ph t hiện lỗi luồng dữ liệu logic.
Một số lỗi khi lập tr nh là do s dụng dữ liệu sai và ở c c vị tr chƣa đ ng. Hệ
thống kiểu t y theo chƣơng tr nh mà phân vùng gi trị hợp lệ và kiểm tra ở thời điểm
ch y chƣơng tr nhxem ph n v ng này đ th a m n chƣa. Nhờ vậy, lập tr nh viên c
thể ph t hiện lỗi khi ch y chƣơng tr nh.
b. Tr u tƣ ng h a
C c c c thành phần trong một chƣơng tr nh đƣợc trừu tƣợng hóa bởi một số
kiểu dữ liệu. C c kiểu dữ liệu trừu tƣợng (ADT- Abstract Data Type), là cơ sở để định
16
nghĩa c c kiểu dữ liệu mới giấu đi cấu tr c bên trong của n với các thành phần khác
trong chƣơng tr nh. Nó có thể c c c giao diện cơ bản để ẩn đi thông tin và h n chế sự
phụ thuộc vào c c module kh c. C c ngôn ngữ hƣớng đối tƣợng thƣờng s dụng c c
kiểu dữ liệu trừu tƣợng.
c. Làm tài iệu
Trong nhiều ngôn ngữ kiểu tĩnh ví dụ C, một số thành phần của chƣơng tr nh
đ i h i ngƣời lập tr nh phải ch th ch kiểu thông tin. V dụ trong C biến phải đƣợc b o
kiểu gi trị, mảng phải đƣợc khai báo kiểu mảng và k ch thƣớc tối đa c c định nghĩa
hàm phải đƣợc khai b o kiểu trả về và kiểu của c c đối số.
d. Tăng hiệu quả
Một chƣơng tr nh đƣợc cho là định kiểu tốt (well-typed) sẽ cung cấp thông tin
cho tr nh biên dịch, giúp trình biên dịch cải thiện qu tr nh dịch chƣơng tr nh. Đối với
c c biến c kiểu tĩnh vị tr thể hiện trong m m y của c c biến này c thể đƣợc quyết
định bởi trình biên dịch. Việc này rất có giá trị khi một biến chỉ c thể có một kiểu gi
trị cố định.
Trong lĩnh vực bảo mật m ng, hệ thống kiểu đƣợc s dụng để xác minh các giao
thức, cấu trúc thông tin trên web đặc biệt trong nhân của một số mô hình bảo mật nhƣ
Java hay JINI.
Ví dụ về hệ thống kiểu trong một trình biên dịch
Hình 2.1 Hệ thống kiểu trong trinh biên dịch
Một trình biên dịch thƣờng có 3 tr ng thái chính: scanning, syntatic analysis và
type analysis tƣơng ứng với 3 chức năng : scanner parser và type checker. Trong đ
hệ thống kiểu sẽ nằm trong bộ Semantic subroutine, mà type checker là một thành
phần trong đ . Với đầu vào là một chƣơng tr nh đƣợc viết bằng một ngôn ngữ lập trình
cụ thể, scanner sẽ s dụng hữu h n các tr ng thái và ánh x chuỗi kí tự thu đƣợc từ
đầu vào bảng TOKEN. Tiếp theo bảng TOKEN này sẽ đƣợc ánh x sang một cấu trúc
trừu tƣợng nhờ có bộ parser. Bộ kiểm tra kiểu typechecker sẽ kiểm tra xem chƣơng
tr nh c là định kiểu tốt hay không.
17
2.2. Giao dịch và bộ nhớ giao dịch phần mềm ( Software Transactional Memory-
STM)
2.2.1. Giao dịch (Transaction)
Một giao dịch là một luồng điều khiển mà áp dụng một chuỗi hữu h n các thao
tác nguyên thủy (primitive) vào bộ nhớ [8]. Hay nói cách khác một giao dịch là một
thực thi của một chƣơng tr nh ngƣời dùng.
Các hệ quản trị cơ sở dữ liệu là một thể hiện điển hình cho các giao dịch trong
các hệ thống phần mềm lớn.
Giao dịch có 4 tính chất và đƣợc viết tắt ACID nhƣ sau :
a. Tính nguyên t (Atomicity): Một giao dịch là một tập c c thao t c đƣợc thực
hiện hoặc toàn bộ, hoặc không thực hiện gì cả.
b. Tính nhất quán (Consistency): Mỗi giao dịch đƣợc thực thi không đƣợc tranh
chấp với các giao dịch khác.
c. T nh độc lập (Isolation): Ngƣời dùng có thể hiểu đƣợc một giao dịch mà không
cần phải xem xét ảnh hƣởng của các giao dịch tƣơng tranh kh c đang ch y.
d. Tính bền vững (Durability): Sau khi giao dịch đ hoàn toàn thành công c c
tr ng thái của n đƣợc duy trì ngay cả khi hệ thống gặp sự cố.
Các tr ng thái của một giao dịch bao gồm:
Ho t động (Active): Giao dịch giữ tr ng th i này trong khi n đang thực
hiện.
Đ ng bộ phận (Partially Committed): Sau khi lệnh cuối c ng đƣợc thực
hiện.
Thất b i (Failed) : Khi giao dịch không thể tiếp tục thực hiện đƣợc
Hủy b (Aborted): Nếu giao dịch gặp tr ng thái thất b i th sau đ giao
dịch cần phải khôi phục l i tr ng thái của n trƣớc khi khởi động giao
dịch. Hủy b là kết quả cuối của qu tr nh đ .
Committed: Sau khi giao dịch hoàn toàn thành công, nó sẽ đi vào tr ng
thái này.
Hình 2.2 Các trạng thái của giao dịch
18
Tải về để xem bản đầy đủ
53 trang
16960
Free
Bạn đang xem 20 trang mẫu của tài liệu "Luận văn Tính cận trên bộ nhớ log của chương trình sử dụng giao dịch", để tải tài liệu gốc về máy hãy click vào nút Download ở trên
File đính kèm:
- luan_van_tinh_can_tren_bo_nho_log_cua_chuong_trinh_su_dung_g.pdf
